Re: [isabelle] lexical matters
On Tue, 18 Jan 2011, mark at proof-technologies.com wrote:
Dvid Matthews kindly provides ways in Poly/ML to manage the whole
compilation process in user space, including printing and binding of
the results. One would merely have to protect agains shadowing of
certain structure names, say.
Oh good. This is excellent news. How long has this been available for?
Maybe 2 years. It was one of the many improvements that David Matthews
did for parallel ML and ML IDE support.
This is where the Isabelle/ML compiler invocation happens:
It is basically the Isabelle/Isar toplevel running ML, with toplevel name
space management and pretty printing under our control. Without that
parallel Isabelle would hardly work in practice.
This archive was generated by a fusion of
Pipermail (Mailman edition) and