added some proof state markup, notably number of subgoals (e.g. for indentation);
tuned;
--- 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";
--- 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"
--- 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 ***)
--- 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 *)