[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 14:08:40 CEST 2014
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
More information about the isabelle-dev