# HG changeset patch
# User wenzelm
# Date 1436358600 -7200
# Node ID 044f8bb3dd30c44abe8f65822484c3210f4be57a
# Parent  896704918a1fdac73529a989f2fbed4d9404f474
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;

diff -r 896704918a1f -r 044f8bb3dd30 src/Pure/Isar/isar_cmd.ML
--- 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;
diff -r 896704918a1f -r 044f8bb3dd30 src/Pure/Isar/isar_syn.ML
--- 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));
 
 
 
diff -r 896704918a1f -r 044f8bb3dd30 src/Pure/Isar/keyword.ML
--- 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];
 
diff -r 896704918a1f -r 044f8bb3dd30 src/Pure/Isar/outer_syntax.ML
--- 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, ...}) =>
diff -r 896704918a1f -r 044f8bb3dd30 src/Pure/Isar/toplevel.ML
--- 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));