cannot_undo;
authorwenzelm
Wed May 26 22:43:50 1999 +0200 (1999-05-26 ago)
changeset 6734151c07f5b70a
parent 6733 429bbd7ef26d
child 6735 e5138b3dbd3b
cannot_undo;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed May 26 22:43:27 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed May 26 22:43:50 1999 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val exit: Toplevel.transition -> Toplevel.transition
     1.5    val restart: Toplevel.transition -> Toplevel.transition
     1.6    val quit: Toplevel.transition -> Toplevel.transition
     1.7 +  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.8    val clear_undo: Toplevel.transition -> Toplevel.transition
     1.9    val undo: Toplevel.transition -> Toplevel.transition
    1.10    val redo: Toplevel.transition -> Toplevel.transition
    1.11 @@ -56,6 +57,8 @@
    1.12  
    1.13  (* history commands *)
    1.14  
    1.15 +fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    1.16 +
    1.17  val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    1.18  val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    1.19