added Isar.linear_undo;

--- a/src/Pure/Isar/isar.ML	Thu Jul 10 17:47:40 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Thu Jul 10 18:02:34 2008 +0200
@@ -13,6 +13,7 @@
   val goal: unit -> thm
   val >> : Toplevel.transition -> bool
   val >>> : Toplevel.transition list -> unit
+  val linear_undo: int -> unit
   val undo: int -> unit
   val crashes: exn list ref
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
@@ -196,19 +197,21 @@
     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
+fun undo_command id =
+  let val {category, transition, ...} = the_command id in
     (case Toplevel.init_of transition of
-      SOME name => get_prev base before ThyInfo.kill_thy name
-    | NONE => get_prev base)
+      SOME name => get_prev id before ThyInfo.kill_thy name
+    | NONE => get_prev id)
   end;
 
+fun undo_linear id = undo_command (find_command is_proper id);
+fun undo_nested id = undo_command
+  (find_command (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id);
+
 in
 
-fun undo n = change_point (funpow n undo_proper);
+fun linear_undo n = change_point (funpow n undo_linear);
+fun undo n = change_point (funpow n undo_nested);
 
 end;
 

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 10 17:47:40 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 10 18:02:34 2008 +0200
@@ -740,7 +740,12 @@
 (* global Isar state commands *)
 
 val _ =
-  OuterSyntax.improper_command "Isar.undo" "undo tty commands" K.control
+  OuterSyntax.improper_command "Isar.linear_undo" "undo tty commands" K.control
+    (Scan.optional P.nat 1 >>
+      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
+
+val _ =
+  OuterSyntax.improper_command "Isar.undo" "undo tty commands (skipping closed proofs)" K.control
     (Scan.optional P.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));