IsabelleProcess: emit status "ready" after initialization and reports;
authorwenzelm
Tue, 02 Jun 2009 23:30:45 +0200
changeset 31384 ce169bd37fc0
parent 31383 ac7abb2e5944
child 31385 bc1f918ccf68
IsabelleProcess: emit status "ready" after initialization and reports;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/System/isabelle_process.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";
 
 
 
--- 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;