# HG changeset patch
# User wenzelm
# Date 1199052447 -3600
# Node ID 55a458a31e37a58eb992bff10ff647c9a35940cd
# Parent  be58ef74140acc9cd09f8d061699d8d2e1ad93d7
added PROMPT message;

diff -r be58ef74140a -r 55a458a31e37 lib/classes/isabelle/IsabelleProcess.java
--- a/lib/classes/isabelle/IsabelleProcess.java	Sun Dec 30 22:10:20 2007 +0100
+++ b/lib/classes/isabelle/IsabelleProcess.java	Sun Dec 30 23:07:27 2007 +0100
@@ -69,9 +69,9 @@
      */
     public static class Result {
         public enum Kind {
-            STDIN, STDOUT, STDERR, SIGNAL, EXIT,                // Posix channels/events
-            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG,  // Isabelle messages
-            SYSTEM                                              // internal system notification
+            STDIN, STDOUT, STDERR, SIGNAL, EXIT,                        // Posix channels/events
+            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT,  // Isabelle messages
+            SYSTEM                                                      // internal system notification
         };
         public Kind kind;
         public String result;
@@ -92,6 +92,7 @@
               this.kind == Kind.STDIN ||
               this.kind == Kind.SIGNAL ||
               this.kind == Kind.EXIT ||
+              this.kind == Kind.PROMPT ||
               this.kind == Kind.SYSTEM;
         }
 
@@ -307,6 +308,7 @@
                                 case 'D': kind = Result.Kind.WARNING; break;
                                 case 'E': kind = Result.Kind.ERROR; break;
                                 case 'F': kind = Result.Kind.DEBUG; break;
+                                case 'G': kind = Result.Kind.PROMPT; break;
                                 default: kind = Result.Kind.STDOUT; break;
                             }
                         }
diff -r be58ef74140a -r 55a458a31e37 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Sun Dec 30 22:10:20 2007 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Sun Dec 30 23:07:27 2007 +0100
@@ -21,13 +21,14 @@
 sig
   val test_markupN: string
   val test_markup: Markup.T -> output * output
+  val isabelle_processN: string
   val init: unit -> unit
 end;
 
 structure IsabelleProcess: ISABELLE_PROCESS =
 struct
 
-(* test markup *)
+(* test_markup *)
 
 val test_markupN = "test_markup";
 
@@ -40,6 +41,8 @@
 
 (* channels *)
 
+val isabelle_processN = "isabelle_process";
+
 local
 
 fun special c = chr 2 ^ c;
@@ -58,6 +61,10 @@
   Output.error_fn    := output "E" Markup.error;
   Output.debug_fn    := output "F" Markup.debug);
 
+val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
+  if name = Markup.promptN then (special "G", special_end ^ "\n")
+  else ("", ""));
+
 end;
 
 
@@ -66,6 +73,7 @@
 fun init () =
  (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
   setup_channels ();
+  change print_mode (update (op =) isabelle_processN);
   Isar.secure_main ());
 
 end;