src/Pure/General/markup.ML

--- a/src/Pure/General/markup.ML	Wed Aug 25 20:43:03 2010 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 25 21:31:22 2010 +0200
@@ -99,6 +99,8 @@
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
+  val subgoalsN: string
+  val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
@@ -156,16 +158,13 @@
 fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
 
 
-(* name *)
+(* misc properties *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
 val (bindingN, binding) = markup_string "binding" nameN;
 
-
-(* kind *)
-
 val kindN = "kind";
 
 
@@ -305,6 +304,9 @@
 
 (* toplevel *)
 
+val subgoalsN = "subgoals";
+val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
+
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
 val (sendbackN, sendback) = markup_elem "sendback";