# HG changeset patch
# User wenzelm
# Date 1243978245 -7200
# Node ID ce169bd37fc0cd72dd621c254581935197b48f7b
# Parent  ac7abb2e5944be27e940beea03a0a39b1df9909d
IsabelleProcess: emit status "ready" after initialization and reports;

diff -r ac7abb2e5944 -r ce169bd37fc0 src/Pure/General/markup.ML
--- 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";
 
 
 
diff -r ac7abb2e5944 -r ce169bd37fc0 src/Pure/General/markup.scala
--- 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 */
 
diff -r ac7abb2e5944 -r ce169bd37fc0 src/Pure/System/isabelle_process.ML
--- 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;