[isabelle-dev] Hints on Isabelle/ML IDE

[Makarius]

The Isabelle/ML IDE is getting more and more useful.

Working on main HOL is technically easy:

   isabelle jedit -l Pure Main.thy

Then any of the auxiliary ML files can be opened.  It merely requires 
sufficient resources if they are active in large numbers.


For Pure this is less immediate, due to the delicate bootstrap process.
The Prover IDE is only fully functional after Pure.thy is done, so it is 
too late for itself.

What works is the following indirection, via some auxiliary theory (e.g. 
see the attachment):

   isabelle jedit -l Pure Test.thy

Here a few ML files of Pure are loaded on top of itself -- a second time. 
This allows to shed some light (with colors) on otherwise grey ML sources. 
It is particularly useful for challenging modules like locale or 
local_theory infrastructure: with inferred types it becomes easier to see 
what goes on.

We are all getting older, and need tools for what we could do on the spot 
10-20 years ago.  In the early 1990-ies there was not even syntax 
highlighting for ML in the editor, and no ML compiler running on regular 
hardware in the first place.


 	Makarius
-------------- next part --------------
theory Test imports Pure
begin

ML_file "General/name_space.ML"

end