--- 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;
}
}
--- 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;