# HG changeset patch
# User wenzelm
# Date 927751430 -7200
# Node ID 151c07f5b70a6a17f73a10c1906d1ba625804556
# Parent  429bbd7ef26dd785ffe8a05c026cef2dba1a1b6c
cannot_undo;

diff -r 429bbd7ef26d -r 151c07f5b70a src/Pure/Isar/isar_cmd.ML
--- 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;