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: http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-2/src/Pure/ML/ml_compiler_polyml-5.3.ML 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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.