src/Pure/Isar/isar_cmd.ML
changeset 6734 151c07f5b70a
parent 6694 335833a8b10a
child 6742 6b5cb872d997
--- a/src/Pure/Isar/isar_cmd.ML	Wed May 26 22:43:27 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed May 26 22:43:50 1999 +0200
@@ -11,6 +11,7 @@
   val exit: Toplevel.transition -> Toplevel.transition
   val restart: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
+  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undo: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
@@ -56,6 +57,8 @@
 
 (* history commands *)
 
+fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
+
 val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;