# HG changeset patch
# User wenzelm
# Date 1281445965 -7200
# Node ID bb2df73fab2c7e8a7a0a2dcceb2eac57cd64e475
# Parent  4863a3816fc106f9c2802a433454978ece569a06
removed obsolete methods for (ML) commands;

diff -r 4863a3816fc1 -r bb2df73fab2c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Aug 10 14:24:13 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Aug 10 15:12:45 2010 +0200
@@ -342,15 +342,6 @@
     command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   }
 
-  def command(text: String) = input("Isabelle.command " + Isabelle_Syntax.encode_string(text))
-
-  def command(props: List[(String, String)], text: String) =
-    input("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
-      Isabelle_Syntax.encode_string(text))
-
-  def ML_val(text: String) = input("ML_val " + Isabelle_Syntax.encode_string(text))
-  def ML_command(text: String) = input("ML_command " + Isabelle_Syntax.encode_string(text))
-
   def close() = synchronized {    // FIXME avoid synchronized
     command_input ! Close
     closing = true