support for command status;

--- a/src/Pure/General/markup.ML	Tue Jul 15 14:15:49 2008 +0200
+++ b/src/Pure/General/markup.ML	Tue Jul 15 15:46:41 2008 +0200
@@ -67,6 +67,11 @@
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
   val hiliteN: string val hilite: T
+  val unprocessedN: string val unprocessed: T
+  val runningN: string val running: T
+  val finishedN: string val finished: T
+  val failedN: string val failed: T
+  val disposedN: string val disposed: T
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -194,6 +199,15 @@
 val (hiliteN, hilite) = markup_elem "hilite";
 
 
+(* command status *)
+
+val (unprocessedN, unprocessed) = markup_elem "unprocessed";
+val (runningN, running) = markup_elem "running";
+val (finishedN, finished) = markup_elem "finished";
+val (failedN, failed) = markup_elem "failed";
+val (disposedN, disposed) = markup_elem "disposed";
+
+
 (* print mode operations *)
 
 fun default_output (_: T) = ("", "");

--- a/src/Pure/Isar/isar.ML	Tue Jul 15 14:15:49 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Tue Jul 15 15:46:41 2008 +0200
@@ -84,6 +84,10 @@
 fun map_status f = map_command (fn (category, transition, status) =>
   (category, transition, f status));
 
+fun status_markup Initial = Markup.unprocessed
+  | status_markup (Result (_, NONE)) = Markup.finished
+  | status_markup (Result (_, SOME _)) = Markup.failed;
+
 
 (* global collection of identified commands *)
 
@@ -125,13 +129,18 @@
   | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
 
 val the_state = #1 o the_result;
+val command_status = Toplevel.status o #transition o the_command;
+
 
 fun new_command prev (id, cmd) =
   change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id));
 
-fun dispose_command id = change_commands (Graph.del_nodes [id]);
+fun dispose_command id =
+  (command_status id Markup.disposed; change_commands (Graph.del_nodes [id]));
 
-fun change_command_status id f = change_commands (Graph.map_node id (map_status f));
+fun update_command_status id status =
+ (change_commands (Graph.map_node id (map_status (K status)));
+  command_status id (status_markup status));
 
 
 
@@ -180,7 +189,7 @@
     (case Toplevel.transition true tr prev_state of
       NONE => (dispose_command id; false)
     | SOME (result as (_, err)) =>
-        (change_command_status id (K (Result result));
+        (update_command_status id (Result result);
           Option.map (Toplevel.error_msg tr) err;
           if is_some err orelse category = Control then dispose_command id
           else set_point id;

--- a/src/Pure/Isar/toplevel.ML	Tue Jul 15 14:15:49 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 15 15:46:41 2008 +0200
@@ -84,6 +84,7 @@
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
+  val status: transition -> Markup.T -> unit
   val error_msg: transition -> exn * string -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: transition
@@ -598,6 +599,9 @@
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;
 
+fun status tr m =
+  setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
+
 fun error_msg tr exn_info =
   setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();