# HG changeset patch
# User wenzelm
# Date 1215703585 -7200
# Node ID ee2721e9e900637b00744eaa7a5bfa8d3c672ff3
# Parent  cd95da386e9a521d557437e867722520e7594b0c
added Isar.undo, which emulates old-style undo on global tty state;

diff -r cd95da386e9a -r ee2721e9e900 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 10 17:26:23 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 10 17:26:25 2008 +0200
@@ -737,6 +737,14 @@
         handle ERROR msg => Scan.fail_with (K msg)));
 
 
+(* global Isar state commands *)
+
+val _ =
+  OuterSyntax.improper_command "Isar.undo" "undo tty commands" K.control
+    (Scan.optional P.nat 1 >>
+      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
+
+
 
 (** diagnostic commands (for interactive mode only) **)