Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cannot_undo;
authorwenzelm
Wed, 26 May 1999 22:43:50 +0200
changeset 6734 151c07f5b70a
parent 6733 429bbd7ef26d
child 6735 e5138b3dbd3b
cannot_undo;
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle