Isabelle/ML snippet syntax problem

[makarius]

Trying to work with Isabelle/ML, I've produced an external file like this:

theory Test_ML
imports Main
begin

ML ‹
(** begin #isabelle-ml *)
(** end #isabelle-ml *)
›

end

This does not quite work: the system prints some undefined things and produces non-sense.

Admittedly, this approach stretches the meta-comment feature a bit far.

[martinring]

This is related to #14, ML is disabled.

The issue with cobra here is, that it doesn't work with empty snippets right now. It should at least not produce nonsense, when using this:

theory Test_ML
imports Main
begin

ML ‹
(** begin #isabelle-ml *)

(** end #isabelle-ml *)
›

end

[martinring]

Part of #16