[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

>  * Writing tools in ML (ML-blocks in thy-file)

Just a side remark: in the repository version we are talking about, and 
thus the coming release, ML in auxiliary files works smoothly and often 
better than the ML blocks, because the file gets its own ML mode.

There is nothing wrong about ML blocks, just an equal balance between 'ML' 
and 'ML_file' to choose whatever fits best the size of the ML code module.


 	Makarius