1.1 --- a/src/Pure/General/markup.ML	Wed Aug 25 20:43:03 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Aug 25 21:31:22 2010 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4    val command_spanN: string val command_span: string -> T
     1.5    val ignored_spanN: string val ignored_span: T
     1.6    val malformed_spanN: string val malformed_span: T
     1.7 +  val subgoalsN: string
     1.8 +  val proof_stateN: string val proof_state: int -> T
     1.9    val stateN: string val state: T
    1.10    val subgoalN: string val subgoal: T
    1.11    val sendbackN: string val sendback: T
    1.12 @@ -156,16 +158,13 @@
    1.13  fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
    1.14  
    1.15  
    1.16 -(* name *)
    1.17 +(* misc properties *)
    1.18  
    1.19  val nameN = "name";
    1.20  fun name a = properties [(nameN, a)];
    1.21  
    1.22  val (bindingN, binding) = markup_string "binding" nameN;
    1.23  
    1.24 -
    1.25 -(* kind *)
    1.26 -
    1.27  val kindN = "kind";
    1.28  
    1.29  
    1.30 @@ -305,6 +304,9 @@
    1.31  
    1.32  (* toplevel *)
    1.33  
    1.34 +val subgoalsN = "subgoals";
    1.35 +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
    1.36 +
    1.37  val (stateN, state) = markup_elem "state";
    1.38  val (subgoalN, subgoal) = markup_elem "subgoal";
    1.39  val (sendbackN, sendback) = markup_elem "sendback";

     2.1 --- a/src/Pure/General/markup.scala	Wed Aug 25 20:43:03 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Wed Aug 25 21:31:22 2010 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4    val Empty = Markup("", Nil)
     2.5  
     2.6  
     2.7 -  /* name */
     2.8 +  /* misc properties */
     2.9  
    2.10    val NAME = "name"
    2.11    val KIND = "kind"
    2.12 @@ -188,6 +188,9 @@
    2.13  
    2.14    /* toplevel */
    2.15  
    2.16 +  val SUBGOALS = "subgoals"
    2.17 +  val PROOF_STATE = "proof_state"
    2.18 +
    2.19    val STATE = "state"
    2.20    val SUBGOAL = "subgoal"
    2.21    val SENDBACK = "sendback"

     3.1 --- a/src/Pure/Isar/proof.ML	Wed Aug 25 20:43:03 2010 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Wed Aug 25 21:31:22 2010 +0200
     3.3 @@ -42,6 +42,7 @@
     3.4    val raw_goal: state -> {context: context, facts: thm list, goal: thm}
     3.5    val goal: state -> {context: context, facts: thm list, goal: thm}
     3.6    val simple_goal: state -> {context: context, goal: thm}
     3.7 +  val status_markup: state -> Markup.T
     3.8    val let_bind: (term list * term) list -> state -> state
     3.9    val let_bind_cmd: (string list * string) list -> state -> state
    3.10    val write: Syntax.mode -> (term * mixfix) list -> state -> state
    3.11 @@ -520,6 +521,11 @@
    3.12      val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
    3.13    in {context = ctxt, goal = goal} end;
    3.14  
    3.15 +fun status_markup state =
    3.16 +  (case try goal state of
    3.17 +    SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
    3.18 +  | NONE => Markup.empty);
    3.19 +
    3.20  
    3.21  
    3.22  (*** structured proof commands ***)

     4.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 25 20:43:03 2010 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 25 21:31:22 2010 +0200
     4.3 @@ -563,13 +563,6 @@
     4.4  fun status tr m =
     4.5    setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
     4.6  
     4.7 -fun async_state (tr as Transition {print, ...}) st =
     4.8 -  if print then
     4.9 -    ignore
    4.10 -      (Future.fork (fn () =>
    4.11 -          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
    4.12 -  else ();
    4.13 -
    4.14  fun error_msg tr exn_info =
    4.15    setmp_thread_position tr (fn () =>
    4.16      Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
    4.17 @@ -628,6 +621,22 @@
    4.18  
    4.19  (* managed execution *)
    4.20  
    4.21 +local
    4.22 +
    4.23 +fun async_state (tr as Transition {print, ...}) st =
    4.24 +  if print then
    4.25 +    ignore
    4.26 +      (Future.fork (fn () =>
    4.27 +          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
    4.28 +  else ();
    4.29 +
    4.30 +fun proof_status tr st =
    4.31 +  (case try proof_of st of
    4.32 +    SOME prf => status tr (Proof.status_markup prf)
    4.33 +  | NONE => ());
    4.34 +
    4.35 +in
    4.36 +
    4.37  fun run_command thy_name tr st =
    4.38    (case
    4.39        (case init_of tr of
    4.40 @@ -637,13 +646,18 @@
    4.41        let val int = is_some (init_of tr) in
    4.42          (case transition int tr st of
    4.43            SOME (st', NONE) =>
    4.44 -            (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
    4.45 +           (status tr Markup.finished;
    4.46 +            proof_status tr st';
    4.47 +            if int then () else async_state tr st';
    4.48 +            SOME st')
    4.49          | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    4.50          | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    4.51          | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    4.52        end
    4.53    | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    4.54  
    4.55 +end;
    4.56 +
    4.57  
    4.58  (* nested commands *)
    4.59