eliminated prompt messages;

--- a/src/Pure/Tools/isabelle_process.ML	Sat Oct 04 14:29:45 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Sat Oct 04 14:43:40 2008 +0200
@@ -130,7 +130,7 @@
     Output.warning_fn  := message out_stream "F" Markup.warningN;
     Output.error_fn    := message out_stream "G" Markup.errorN;
     Output.debug_fn    := message out_stream "H" Markup.debugN;
-    Output.prompt_fn   := message out_stream "I" Markup.promptN;
+    Output.prompt_fn   := ignore;
     out_stream
   end;
 

--- a/src/Pure/Tools/isabelle_process.scala	Sat Oct 04 14:29:45 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Oct 04 14:43:40 2008 +0200
@@ -38,7 +38,6 @@
     val WARNING = Value("WARNING")
     val ERROR = Value("ERROR")
     val DEBUG = Value("DEBUG")
-    val PROMPT = Value("PROMPT")
     // messages codes
     val code = Map(
       ('A' : Int) -> Kind.INIT,
@@ -49,7 +48,6 @@
       ('F' : Int) -> Kind.WARNING,
       ('G' : Int) -> Kind.ERROR,
       ('H' : Int) -> Kind.DEBUG,
-      ('I' : Int) -> Kind.PROMPT,
       ('0' : Int) -> Kind.SYSTEM,
       ('1' : Int) -> Kind.STDIN,
       ('2' : Int) -> Kind.STDOUT,
@@ -67,8 +65,7 @@
       kind == STDIN ||
       kind == SIGNAL ||
       kind == EXIT ||
-      kind == STATUS ||
-      kind == PROMPT
+      kind == STATUS
   }
 
   class Result(val kind: Kind.Value, val props: Properties, val result: String) {