--- a/src/Pure/General/markup.ML Tue Jun 02 21:13:47 2009 +0200
+++ b/src/Pure/General/markup.ML Tue Jun 02 23:30:45 2009 +0200
@@ -108,6 +108,7 @@
val pidN: string
val sessionN: string
val promptN: string val prompt: T
+ val readyN: string val ready: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -307,6 +308,7 @@
val sessionN = "session";
val (promptN, prompt) = markup_elem "prompt";
+val (readyN, ready) = markup_elem "ready";
--- a/src/Pure/General/markup.scala Tue Jun 02 21:13:47 2009 +0200
+++ b/src/Pure/General/markup.scala Tue Jun 02 23:30:45 2009 +0200
@@ -163,6 +163,8 @@
val SIGNAL = "signal"
val EXIT = "exit"
+ val READY = "ready"
+
/* content */
--- a/src/Pure/System/isabelle_process.ML Tue Jun 02 21:13:47 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Jun 02 23:30:45 2009 +0200
@@ -133,6 +133,7 @@
(change print_mode (update (op =) isabelle_processN);
setup_channels out |> init_message;
OuterKeyword.report ();
+ Output.status (Markup.markup Markup.ready "");
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
end;