--- 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;
--- 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);
--- 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);
--- 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 *)