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