improved undo / kill operations;
authorwenzelm
Thu May 27 20:45:20 1999 +0200 (1999-05-27 ago)
changeset 67426b5cb872d997
parent 6741 540fc00ec32b
child 6743 5d50225637c8
improved undo / kill operations;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 11:39:44 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 20:45:20 1999 +0200
     1.3 @@ -13,9 +13,12 @@
     1.4    val quit: Toplevel.transition -> Toplevel.transition
     1.5    val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.6    val clear_undo: Toplevel.transition -> Toplevel.transition
     1.7 +  val redo: Toplevel.transition -> Toplevel.transition
     1.8 +  val undos_proof: int -> Toplevel.transition -> Toplevel.transition
     1.9 +  val kill_proof: Toplevel.transition -> Toplevel.transition
    1.10 +  val undo_theory: Toplevel.transition -> Toplevel.transition
    1.11 +  val kill_theory: Toplevel.transition -> Toplevel.transition
    1.12    val undo: Toplevel.transition -> Toplevel.transition
    1.13 -  val redo: Toplevel.transition -> Toplevel.transition
    1.14 -  val undos: int -> Toplevel.transition -> Toplevel.transition
    1.15    val use: string -> Toplevel.transition -> Toplevel.transition
    1.16    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    1.17    val use_mltext: string -> Toplevel.transition -> Toplevel.transition
    1.18 @@ -58,20 +61,22 @@
    1.19  (* history commands *)
    1.20  
    1.21  fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    1.22 -
    1.23  val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    1.24  val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    1.25  
    1.26 -fun undo_proof prf =
    1.27 -  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else ProofHistory.undo prf;
    1.28 +fun undos_proof n = Toplevel.proof (fn prf =>
    1.29 +  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
    1.30  
    1.31 -fun undo_node hist =
    1.32 -  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist;
    1.33 +val kill_proof = Toplevel.history (fn hist =>
    1.34 +  (case History.current hist of
    1.35 +    Toplevel.Theory _ => raise Toplevel.UNDEF
    1.36 +  | Toplevel.Proof _ => History.undo hist));
    1.37  
    1.38 -val undo = Toplevel.kill o Toplevel.history undo_node o Toplevel.proof undo_proof;
    1.39 +val undo_theory = Toplevel.history (fn hist =>
    1.40 +  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.41  
    1.42 -(* FIXME fix *)
    1.43 -fun undos n = Toplevel.history (funpow n History.undo) o Toplevel.proof (funpow n undo_proof);
    1.44 +val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
    1.45 +val undo = kill_theory o undo_theory o undos_proof 1;
    1.46  
    1.47  
    1.48  (* use ML text *)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Thu May 27 11:39:44 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu May 27 20:45:20 1999 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  val kill_excursionP =
     2.6    OuterSyntax.command "kill" "kill current excursion" K.control
     2.7 -    (Scan.succeed (Toplevel.print o Toplevel.kill));
     2.8 +    (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
     2.9  
    2.10  val contextP =
    2.11    OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
    2.12 @@ -320,10 +320,6 @@
    2.13  
    2.14  (* end proof *)
    2.15  
    2.16 -val kill_proofP =
    2.17 -  OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
    2.18 -    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
    2.19 -
    2.20  val qed_withP =
    2.21    OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
    2.22      K.qed_block
    2.23 @@ -363,27 +359,7 @@
    2.24        >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
    2.25  
    2.26  
    2.27 -(* proof history *)
    2.28 -
    2.29 -val cannot_undoP =
    2.30 -  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
    2.31 -    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
    2.32 -
    2.33 -val clear_undoP =
    2.34 -  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
    2.35 -    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
    2.36 -
    2.37 -val undoP =
    2.38 -  OuterSyntax.improper_command "undo" "undo last command" K.control
    2.39 -    (Scan.succeed (Toplevel.print o IsarCmd.undo));
    2.40 -
    2.41 -val redoP =
    2.42 -  OuterSyntax.improper_command "redo" "redo last command" K.control
    2.43 -    (Scan.succeed (Toplevel.print o IsarCmd.redo));
    2.44 -
    2.45 -val undosP =
    2.46 -  OuterSyntax.improper_command "undos" "undo last commands" K.control
    2.47 -    (P.nat >> (fn n => Toplevel.print o IsarCmd.undos n));
    2.48 +(* proof navigation *)
    2.49  
    2.50  val backP =
    2.51    OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
    2.52 @@ -402,6 +378,33 @@
    2.53      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
    2.54  
    2.55  
    2.56 +(* history *)
    2.57 +
    2.58 +val cannot_undoP =
    2.59 +  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
    2.60 +    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
    2.61 +
    2.62 +val clear_undoP =
    2.63 +  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
    2.64 +    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
    2.65 +
    2.66 +val redoP =
    2.67 +  OuterSyntax.improper_command "redo" "redo last command" K.control
    2.68 +    (Scan.succeed (Toplevel.print o IsarCmd.redo));
    2.69 +
    2.70 +val undos_proofP =
    2.71 +  OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
    2.72 +    (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
    2.73 +
    2.74 +val kill_proofP =
    2.75 +  OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
    2.76 +    (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
    2.77 +
    2.78 +val undoP =
    2.79 +  OuterSyntax.improper_command "undo" "undo last command" K.control
    2.80 +    (Scan.succeed (Toplevel.print o IsarCmd.undo));
    2.81 +
    2.82 +
    2.83  
    2.84  (** diagnostic commands (for interactive mode only) **)
    2.85  
    2.86 @@ -528,10 +531,10 @@
    2.87    print_ast_translationP, token_translationP, oracleP,
    2.88    (*proof commands*)
    2.89    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
    2.90 -  thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
    2.91 -  qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
    2.92 -  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
    2.93 -  undosP, backP, prevP, upP, topP,
    2.94 +  thenP, fromP, factsP, beginP, endP, nextP, qed_withP, qedP,
    2.95 +  terminal_proofP, immediate_proofP, default_proofP, refineP,
    2.96 +  then_refineP, proofP, backP, prevP, upP, topP, cannot_undoP,
    2.97 +  clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    2.98    (*diagnostic commands*)
    2.99    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   2.100    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,