# HG changeset patch
# User wenzelm
# Date 1216124143 -7200
# Node ID 6c347b96d9414ed75307d4291ee220b4d90679d3
# Parent  69c00b56fb369b2bc3f9ceadac9ee8223484abf9
added status channel;

diff -r 69c00b56fb36 -r 6c347b96d941 lib/classes/isabelle/IsabelleProcess.java
--- a/lib/classes/isabelle/IsabelleProcess.java	Tue Jul 15 12:13:14 2008 +0200
+++ b/lib/classes/isabelle/IsabelleProcess.java	Tue Jul 15 14:15:43 2008 +0200
@@ -74,9 +74,12 @@
      */
     public static class Result {
         public enum Kind {
-            STDIN, STDOUT, STDERR, SIGNAL, EXIT,                  // Posix channels/events
-            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT,  // Isabelle messages
-            SYSTEM                                              // internal system notification
+            // Posix channels/events
+            STDIN, STDOUT, STDERR, SIGNAL, EXIT,
+            // Isabelle messages
+            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT, STATUS,
+            // internal system notification
+            SYSTEM
         };
         public Kind kind;
         public Properties props;
@@ -100,6 +103,7 @@
               this.kind == Kind.SIGNAL ||
               this.kind == Kind.EXIT ||
               this.kind == Kind.PROMPT ||
+              this.kind == Kind.STATUS ||
               this.kind == Kind.SYSTEM;
         }
 
@@ -375,6 +379,7 @@
                                 case 'F': kind = Result.Kind.DEBUG; break;
                                 case 'G': kind = Result.Kind.PROMPT; break;
                                 case 'H': kind = Result.Kind.INIT; break;
+                                case 'I': kind = Result.Kind.STATUS; break;
                                 default: kind = Result.Kind.STDOUT; break;
                             }
                             props = null;
diff -r 69c00b56fb36 -r 6c347b96d941 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 15 12:13:14 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 15 14:15:43 2008 +0200
@@ -84,6 +84,7 @@
 
 fun setup_messages () =
  (Output.writeln_fn := Output.writeln_default;
+  Output.status_fn := Output.writeln_default;
   Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
   Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
   Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
diff -r 69c00b56fb36 -r 6c347b96d941 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 15 12:13:14 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 15 14:15:43 2008 +0200
@@ -182,6 +182,7 @@
 
 fun setup_messages () =
  (Output.writeln_fn := (fn s => normalmsg Message s);
+  Output.status_fn := (fn _ => ());
   Output.priority_fn := (fn s => normalmsg Status s);
   Output.tracing_fn := (fn s => normalmsg  Tracing s);
   Output.warning_fn := (fn s => errormsg Message Warning s);
diff -r 69c00b56fb36 -r 6c347b96d941 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Tue Jul 15 12:13:14 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Tue Jul 15 14:15:43 2008 +0200
@@ -109,7 +109,8 @@
   Output.warning_fn  := message "D";
   Output.error_fn    := message "E";
   Output.debug_fn    := message "F";
-  Output.prompt_fn   := message "G");
+  Output.prompt_fn   := message "G";
+  Output.status_fn   := message "I");
 
 
 (* init *)