# HG changeset patch
# User wenzelm
# Date 1282764682 -7200
# Node ID ca8b14fa0d0d22a7f5ee37b6c64b45230f4638a7
# Parent  7f8bc335e203e10401feab5a25f48a7fa387ae4c
added some proof state markup, notably number of subgoals (e.g. for indentation);
tuned;

diff -r 7f8bc335e203 -r ca8b14fa0d0d 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";
diff -r 7f8bc335e203 -r ca8b14fa0d0d src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Aug 25 20:43:03 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 25 21:31:22 2010 +0200
@@ -53,7 +53,7 @@
   val Empty = Markup("", Nil)
 
 
-  /* name */
+  /* misc properties */
 
   val NAME = "name"
   val KIND = "kind"
@@ -188,6 +188,9 @@
 
   /* toplevel */
 
+  val SUBGOALS = "subgoals"
+  val PROOF_STATE = "proof_state"
+
   val STATE = "state"
   val SUBGOAL = "subgoal"
   val SENDBACK = "sendback"
diff -r 7f8bc335e203 -r ca8b14fa0d0d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Aug 25 20:43:03 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Aug 25 21:31:22 2010 +0200
@@ -42,6 +42,7 @@
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
+  val status_markup: state -> Markup.T
   val let_bind: (term list * term) list -> state -> state
   val let_bind_cmd: (string list * string) list -> state -> state
   val write: Syntax.mode -> (term * mixfix) list -> state -> state
@@ -520,6 +521,11 @@
     val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
   in {context = ctxt, goal = goal} end;
 
+fun status_markup state =
+  (case try goal state of
+    SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
+  | NONE => Markup.empty);
+
 
 
 (*** structured proof commands ***)
diff -r 7f8bc335e203 -r ca8b14fa0d0d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 25 20:43:03 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 25 21:31:22 2010 +0200
@@ -563,13 +563,6 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
-fun async_state (tr as Transition {print, ...}) st =
-  if print then
-    ignore
-      (Future.fork (fn () =>
-          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
-  else ();
-
 fun error_msg tr exn_info =
   setmp_thread_position tr (fn () =>
     Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
@@ -628,6 +621,22 @@
 
 (* managed execution *)
 
+local
+
+fun async_state (tr as Transition {print, ...}) st =
+  if print then
+    ignore
+      (Future.fork (fn () =>
+          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
+  else ();
+
+fun proof_status tr st =
+  (case try proof_of st of
+    SOME prf => status tr (Proof.status_markup prf)
+  | NONE => ());
+
+in
+
 fun run_command thy_name tr st =
   (case
       (case init_of tr of
@@ -637,13 +646,18 @@
       let val int = is_some (init_of tr) in
         (case transition int tr st of
           SOME (st', NONE) =>
-            (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
+           (status tr Markup.finished;
+            proof_status tr st';
+            if int then () else async_state tr st';
+            SOME st')
         | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
         | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
         | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
       end
   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
 
+end;
+
 
 (* nested commands *)