specific ML_val vs. ML_command;
authorwenzelm
Mon, 05 Jul 2010 22:26:20 +0200
changeset 37712 7f25bf4b4bca
parent 37711 f1ea60bb7754
child 37713 c82cf6e11669
specific ML_val vs. ML_command;
src/Pure/System/isabelle_process.scala
--- 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