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.
Makariustheory Test imports Pure
begin
ML_file "General/name_space.ML"
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
