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



Hi,

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}
›

end

Then the output of the block is not attached to the ML command, but
rather to the "x" in the binding antiquotation.




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