[forgot to copy to the list, in case anyone else is listening]

And another PS on this: I just suggested file load/save hooks, there is also PG's own file protocol which is activate/deactivate scripting, which also have hooks. These might be nicer to use, but the user ought not to change require commands after activating scripting (again you could spot that and give a warning).

This protocol was the simple design that Makarius and I came up with to solve these multiple file issues cleanly in Isabelle, to attempt to have consistent views in the editor and the file system. He is going on to grander sub-file schemes now...

 - D.
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to