[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

> * When theories have inconsistent file/theory name, you will only find
> the error by stepwise going back the chain of "bad theory" -  errors,
> file by file. This is simply tedious. In PG, you got a backtrace in the
> output, and could immediately identify the broken file.

I need to postpone this, to see if there is anything significant behind 
it.  There are indeed slight inconveniences in re-arranging theory file 
names, but I did not see much of that in the past few years of routine use 
of Isabelle/jEdit (e.g. for Isabelle + AFP maintenance).

Note that the Theories panel is the main point to look over a whole 
project, to see its status -- assuming that the basic project structure is 
right.


 	Makarius