3 Mar
2014
3 Mar
'14
6:50 p.m.
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-Sys...
(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_...
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