specific ML_val vs. ML_command;
--- a/src/Pure/System/isabelle_process.scala Mon Jul 05 20:36:39 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Jul 05 22:26:20 2010 +0200
@@ -157,9 +157,12 @@
output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
Isabelle_Syntax.encode_string(text))
- def ML(text: String) =
+ def ML_val(text: String) =
output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
+ def ML_command(text: String) =
+ output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
+
def close() = synchronized { // FIXME watchdog/timeout
output_raw("\u0000")
closing = true