provide old-style undo operation (still unused);
clarified command category;
misc tuning;

--- a/src/Pure/Isar/isar.ML	Thu Jul 10 17:26:22 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Thu Jul 10 17:26:23 2008 +0200
@@ -13,6 +13,7 @@
   val goal: unit -> thm
   val >> : Toplevel.transition -> bool
   val >>> : Toplevel.transition list -> unit
+  val undo: int -> unit
   val crashes: exn list ref
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
@@ -40,20 +41,20 @@
 
 (* command category *)
 
-datatype category = Empty | BeginTheory of string | Theory | Proof | Other;
+datatype category = Empty | Theory | Proof | Diag | Control;
 
 fun category_of tr =
   let val name = Toplevel.name_of tr in
     if name = "" then Empty
-    else
-      (case Toplevel.init_of tr of
-        SOME thy_name => BeginTheory thy_name
-      | NONE =>
-          if OuterKeyword.is_theory name then Theory
-          else if OuterKeyword.is_proof name then Proof
-          else Other)
+    else if OuterKeyword.is_theory name then Theory
+    else if OuterKeyword.is_proof name then Proof
+    else if OuterKeyword.is_diag name then Diag
+    else Control
   end;
 
+val is_theory = fn Theory => true | _ => false;
+val is_proper = fn Theory => true | Proof => true | _ => false;
+
 
 (* datatype command *)
 
@@ -97,8 +98,10 @@
 fun init_commands () = change_commands (K empty_commands);
 
 fun the_command id =
-  if id = no_id then empty_command
-  else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id);
+  let val Command cmd =
+    if id = no_id then empty_command
+    else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id)
+  in cmd end;
 
 fun prev_command id =
   if id = no_id then NONE
@@ -112,11 +115,11 @@
 
 
 fun the_result id =
-  let val Command {transition, status, ...} = the_command id in
-    (case status of
-      Result res => res
-    | _ => error ("Unfinished command " ^ Toplevel.str_of transition))
-  end;
+  (case the_command id of
+    {status = Result res, ...} => res
+  | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
+
+val the_state = #1 o the_result;
 
 fun new_command prev (id, cmd) =
   change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id));
@@ -134,13 +137,15 @@
 local val global_point = ref no_id in
 
 fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f);
-
-fun point_result () = NAMED_CRITICAL "Isar" (fn () =>
-  let val id = ! global_point in (id, the_result id) end);
+fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point);
 
 end;
 
-fun init_point () = change_point (K no_id);
+fun set_point id = change_point (K id);
+fun init_point () = set_point no_id;
+
+fun point_result () = NAMED_CRITICAL "Isar" (fn () =>
+  let val id = point () in (id, the_result id) end);
 
 fun state () = #1 (#2 (point_result ()));
 fun exn () = #2 (#2 (point_result ()));
@@ -156,22 +161,25 @@
 
 (* interactive state transformations --- NOT THREAD-SAFE! *)
 
+fun result_error _ NONE = ()
+  | result_error tr (SOME err) = Toplevel.error_msg tr err;
+
 nonfix >> >>>;
 
 fun >> raw_tr =
   let
     val (id, tr) = identify raw_tr;
     val (prev, (prev_state, _)) = point_result ();
-    val _ = new_command prev (id, make_command (category_of tr, tr, Initial));
+    val category = category_of tr;
+    val _ = new_command prev (id, make_command (category, tr, Initial));
   in
     (case Toplevel.transition true tr prev_state of
       NONE => (dispose_command id; false)
     | SOME result =>
-        (change_command_status id (K (Result result));
-          change_point (K id);
-          (case #2 result of
-            NONE => ()
-          | SOME err => Toplevel.error_msg tr err);
+        (change_command_status id (K (Result result));  (* FIXME outdate all_succs (!?) *)
+          result_error tr (#2 result);
+          if category = Control then dispose_command id
+          else set_point id;
           true))
   end;
 
@@ -179,6 +187,36 @@
   | >>> (tr :: trs) = if >> tr then >>> trs else ();
 
 
+(* old-style navigation *)
+
+local
+
+fun err_undo () = error "Undo history exhausted";
+
+fun get_prev id = the_default no_id (prev_command id);
+
+fun find_command pred id =
+  (case #category (the_command id) of
+    Empty => err_undo ()
+  | category => if pred category then id else find_command pred (get_prev id));
+
+fun undo_proper id =
+  let
+    val base = find_command (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id;
+    val {category, transition, ...} = the_command base;
+  in
+    (case Toplevel.init_of transition of
+      SOME name => get_prev base before ThyInfo.kill_thy name
+    | NONE => get_prev base)
+  end;
+
+in
+
+fun undo n = change_point (funpow n undo_proper);
+
+end;
+
+
 (* toplevel loop *)
 
 val crashes = ref ([]: exn list);
@@ -189,10 +227,11 @@
   let
     fun check_secure () =
       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
-    val (prev, _) = point_result ();
+    val prev = point ();
+    val prev_name = Toplevel.name_of (#transition (the_command prev));
     val prompt_markup =
-      if prev = no_id then I
-      else Markup.markup (Markup.properties [(Markup.idN, prev)] Markup.position);
+      prev <> no_id ? Markup.markup
+        (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt);
   in
     (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
       NONE => if secure then quit () else ()