# HG changeset patch
# User wenzelm
# Date 1278361580 -7200
# Node ID 7f25bf4b4bca3d6ca5188291848167e6968e1f7d
# Parent  f1ea60bb7754dd5119aec0d240cc2b79298769d8
specific ML_val vs. ML_command;

diff -r f1ea60bb7754 -r 7f25bf4b4bca 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