more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
--- a/src/Pure/Isar/isar_cmd.ML Wed Jul 08 12:09:44 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jul 08 14:30:00 2015 +0200
@@ -182,8 +182,6 @@
val local_done_proof = Toplevel.proof Proof.local_done_proof;
val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
-val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
-
(* global endings *)
@@ -194,12 +192,10 @@
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
-val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
-
(* common endings *)
-fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
+fun qed m = local_qed m o global_qed m;
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
val default_proof = local_default_proof o global_default_proof;
val immediate_proof = local_immediate_proof o global_immediate_proof;
--- a/src/Pure/Isar/isar_syn.ML Wed Jul 08 12:09:44 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 08 14:30:00 2015 +0200
@@ -674,9 +674,7 @@
val _ =
Outer_Syntax.command @{command_keyword proof} "backward proof step"
(Scan.option Method.parse >> (fn m =>
- (Option.map Method.report m;
- Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
- Toplevel.skip_proof (fn i => i + 1))));
+ (Option.map Method.report m; Toplevel.proofs (Proof.proof_results m))));
(* subgoal focus *)
@@ -715,7 +713,7 @@
Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
(Scan.succeed
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
- Toplevel.skip_proof (fn h => (report_back (); h))));
+ Toplevel.skip_proof report_back));
--- a/src/Pure/Isar/keyword.ML Wed Jul 08 12:09:44 2015 +0200
+++ b/src/Pure/Isar/keyword.ML Wed Jul 08 14:30:00 2015 +0200
@@ -62,6 +62,8 @@
val is_proof_goal: keywords -> string -> bool
val is_qed: keywords -> string -> bool
val is_qed_global: keywords -> string -> bool
+ val is_proof_open: keywords -> string -> bool
+ val is_proof_close: keywords -> string -> bool
val is_proof_asm: keywords -> string -> bool
val is_improper: keywords -> string -> bool
val is_printed: keywords -> string -> bool
@@ -255,6 +257,10 @@
val is_qed = command_category [qed, qed_script, qed_block];
val is_qed_global = command_category [qed_global];
+val is_proof_open =
+ command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open];
+val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
+
val is_proof_asm = command_category [prf_asm, prf_asm_goal];
val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 08 12:09:44 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 08 14:30:00 2015 +0200
@@ -172,8 +172,14 @@
fun parse_command thy =
Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
let
+ val keywords = Thy_Header.get_keywords thy;
val command_tags = Parse.command_ -- Parse.tags;
- val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
+ val tr0 =
+ Toplevel.empty
+ |> Toplevel.name name
+ |> Toplevel.position pos
+ |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
+ |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
in
(case lookup_commands thy name of
SOME (Command {command_parser = Parser parse, ...}) =>
--- a/src/Pure/Isar/toplevel.ML Wed Jul 08 12:09:44 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 08 14:30:00 2015 +0200
@@ -69,8 +69,9 @@
val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
val proof: (Proof.state -> Proof.state) -> transition -> transition
val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
- val skip_proof: (int -> int) -> transition -> transition
- val skip_proof_to_theory: (int -> bool) -> transition -> transition
+ val skip_proof: (unit -> unit) -> transition -> transition
+ val skip_proof_open: transition -> transition
+ val skip_proof_close: transition -> transition
val exec_id: Document_ID.exec -> transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val add_hook: (transition -> state -> state -> unit) -> unit
@@ -510,16 +511,24 @@
val proofs = proofs' o K;
val proof = proof' o K;
+
+(* skipped proofs *)
+
fun actual_proof f = transaction (fn _ =>
(fn Proof (prf, x) => Proof (f prf, x)
| _ => raise UNDEF));
fun skip_proof f = transaction (fn _ =>
- (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
+ (fn skip as Skipped_Proof _ => (f (); skip)
| _ => raise UNDEF));
-fun skip_proof_to_theory pred = transaction (fn _ =>
- (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
+val skip_proof_open = transaction (fn _ =>
+ (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x)
+ | _ => raise UNDEF));
+
+val skip_proof_close = transaction (fn _ =>
+ (fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
+ | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x)
| _ => raise UNDEF));