On Mon, 3 Mar 2014, Makarius wrote:
(1) short version (Isabelle/Pure bootstrap):
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/compiler_polyml.ML#l40
(2) long version (full Isabelle/ML managed compilation with IDE markup)
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML/ml_compiler_polyml.ML#l184
In both cases, the critical bit is the two-stage invocation of
PolyML.compiler: first the static then the dynamic phase.
That was 1 second too quick: PolyML.Compiler.CPCompilerResultFun is where
the two phases can be intercepted.
David can explain better what is what in PolyML.Compiler, if this is
required here.
Makarius
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
