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