Re: [isabelle] Isabelle2014-RC2 issues: Output markup for ML-blocks

On 07.08.2014 10:09, Lars Noschinski wrote:

consider the following code:

theory Scratch imports Pure begin

ML ‹
val x = 1
val y = yield_singleton Proof_Context.read_vars (@{binding x}, NONE,
NoSyn) @{context}


Then the output of the block is not attached to the ML command, but
rather to the "x" in the binding antiquotation.
The same happens even with just

ML ‹ @{binding x} ›


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