specific ML_val vs. ML_command;
1.1 --- a/src/Pure/System/isabelle_process.scala Mon Jul 05 20:36:39 2010 +0200
1.2 +++ b/src/Pure/System/isabelle_process.scala Mon Jul 05 22:26:20 2010 +0200
1.3 @@ -157,9 +157,12 @@
1.4 output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
1.5 Isabelle_Syntax.encode_string(text))
1.6
1.7 - def ML(text: String) =
1.8 + def ML_val(text: String) =
1.9 output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
1.10
1.11 + def ML_command(text: String) =
1.12 + output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
1.13 +
1.14 def close() = synchronized { // FIXME watchdog/timeout
1.15 output_raw("\u0000")
1.16 closing = true