[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...
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.