src/Pure/Isar/isar_cmd.ML
changeset 6734 151c07f5b70a
parent 6694 335833a8b10a
child 6742 6b5cb872d997
equal deleted inserted replaced
6733:429bbd7ef26d 6734:151c07f5b70a
     9 sig
     9 sig
    10   val break: Toplevel.transition -> Toplevel.transition
    10   val break: Toplevel.transition -> Toplevel.transition
    11   val exit: Toplevel.transition -> Toplevel.transition
    11   val exit: Toplevel.transition -> Toplevel.transition
    12   val restart: Toplevel.transition -> Toplevel.transition
    12   val restart: Toplevel.transition -> Toplevel.transition
    13   val quit: Toplevel.transition -> Toplevel.transition
    13   val quit: Toplevel.transition -> Toplevel.transition
       
    14   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    14   val clear_undo: Toplevel.transition -> Toplevel.transition
    15   val clear_undo: Toplevel.transition -> Toplevel.transition
    15   val undo: Toplevel.transition -> Toplevel.transition
    16   val undo: Toplevel.transition -> Toplevel.transition
    16   val redo: Toplevel.transition -> Toplevel.transition
    17   val redo: Toplevel.transition -> Toplevel.transition
    17   val undos: int -> Toplevel.transition -> Toplevel.transition
    18   val undos: int -> Toplevel.transition -> Toplevel.transition
    18   val use: string -> Toplevel.transition -> Toplevel.transition
    19   val use: string -> Toplevel.transition -> Toplevel.transition
    53 val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    54 val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    54 val quit = Toplevel.imperative quit;
    55 val quit = Toplevel.imperative quit;
    55 
    56 
    56 
    57 
    57 (* history commands *)
    58 (* history commands *)
       
    59 
       
    60 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    58 
    61 
    59 val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    62 val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    60 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    63 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    61 
    64 
    62 fun undo_proof prf =
    65 fun undo_proof prf =