--- a/src/Pure/General/markup.ML Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/markup.ML Tue Aug 31 23:28:21 2010 +0200
@@ -14,8 +14,8 @@
val properties: Properties.T -> T -> T
val nameN: string
val name: string -> T -> T
+ val kindN: string
val bindingN: string val binding: string -> T
- val kindN: string
val entityN: string val entity: string -> T
val defN: string
val refN: string
@@ -118,6 +118,7 @@
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
+ val reportN: string val report: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -164,13 +165,12 @@
val nameN = "name";
fun name a = properties [(nameN, a)];
-val (bindingN, binding) = markup_string "binding" nameN;
-
val kindN = "kind";
(* formal entities *)
+val (bindingN, binding) = markup_string "binding" nameN;
val (entityN, entity) = markup_string "entity" nameN;
val defN = "def";
@@ -343,6 +343,8 @@
val (promptN, prompt) = markup_elem "prompt";
val (readyN, ready) = markup_elem "ready";
+val (reportN, report) = markup_elem "report";
+
(** print mode operations **)