more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
authorwenzelm
Wed Jul 08 14:30:00 2015 +0200 (2015-07-08 ago)
changeset 60695044f8bb3dd30
parent 60694 896704918a1f
child 60696 b3fa4a8cdb5f
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 08 12:09:44 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 08 14:30:00 2015 +0200
     1.3 @@ -182,8 +182,6 @@
     1.4  val local_done_proof = Toplevel.proof Proof.local_done_proof;
     1.5  val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
     1.6  
     1.7 -val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
     1.8 -
     1.9  
    1.10  (* global endings *)
    1.11  
    1.12 @@ -194,12 +192,10 @@
    1.13  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
    1.14  val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
    1.15  
    1.16 -val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
    1.17 -
    1.18  
    1.19  (* common endings *)
    1.20  
    1.21 -fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
    1.22 +fun qed m = local_qed m o global_qed m;
    1.23  fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
    1.24  val default_proof = local_default_proof o global_default_proof;
    1.25  val immediate_proof = local_immediate_proof o global_immediate_proof;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 08 12:09:44 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 08 14:30:00 2015 +0200
     2.3 @@ -674,9 +674,7 @@
     2.4  val _ =
     2.5    Outer_Syntax.command @{command_keyword proof} "backward proof step"
     2.6      (Scan.option Method.parse >> (fn m =>
     2.7 -      (Option.map Method.report m;
     2.8 -        Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
     2.9 -        Toplevel.skip_proof (fn i => i + 1))));
    2.10 +      (Option.map Method.report m; Toplevel.proofs (Proof.proof_results m))));
    2.11  
    2.12  
    2.13  (* subgoal focus *)
    2.14 @@ -715,7 +713,7 @@
    2.15    Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
    2.16      (Scan.succeed
    2.17       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
    2.18 -      Toplevel.skip_proof (fn h => (report_back (); h))));
    2.19 +      Toplevel.skip_proof report_back));
    2.20  
    2.21  
    2.22  
     3.1 --- a/src/Pure/Isar/keyword.ML	Wed Jul 08 12:09:44 2015 +0200
     3.2 +++ b/src/Pure/Isar/keyword.ML	Wed Jul 08 14:30:00 2015 +0200
     3.3 @@ -62,6 +62,8 @@
     3.4    val is_proof_goal: keywords -> string -> bool
     3.5    val is_qed: keywords -> string -> bool
     3.6    val is_qed_global: keywords -> string -> bool
     3.7 +  val is_proof_open: keywords -> string -> bool
     3.8 +  val is_proof_close: keywords -> string -> bool
     3.9    val is_proof_asm: keywords -> string -> bool
    3.10    val is_improper: keywords -> string -> bool
    3.11    val is_printed: keywords -> string -> bool
    3.12 @@ -255,6 +257,10 @@
    3.13  val is_qed = command_category [qed, qed_script, qed_block];
    3.14  val is_qed_global = command_category [qed_global];
    3.15  
    3.16 +val is_proof_open =
    3.17 +  command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open];
    3.18 +val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
    3.19 +
    3.20  val is_proof_asm = command_category [prf_asm, prf_asm_goal];
    3.21  val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
    3.22  
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 08 12:09:44 2015 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 08 14:30:00 2015 +0200
     4.3 @@ -172,8 +172,14 @@
     4.4  fun parse_command thy =
     4.5    Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
     4.6      let
     4.7 +      val keywords = Thy_Header.get_keywords thy;
     4.8        val command_tags = Parse.command_ -- Parse.tags;
     4.9 -      val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
    4.10 +      val tr0 =
    4.11 +        Toplevel.empty
    4.12 +        |> Toplevel.name name
    4.13 +        |> Toplevel.position pos
    4.14 +        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
    4.15 +        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
    4.16      in
    4.17        (case lookup_commands thy name of
    4.18          SOME (Command {command_parser = Parser parse, ...}) =>
     5.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jul 08 12:09:44 2015 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 08 14:30:00 2015 +0200
     5.3 @@ -69,8 +69,9 @@
     5.4    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
     5.5    val proof: (Proof.state -> Proof.state) -> transition -> transition
     5.6    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
     5.7 -  val skip_proof: (int -> int) -> transition -> transition
     5.8 -  val skip_proof_to_theory: (int -> bool) -> transition -> transition
     5.9 +  val skip_proof: (unit -> unit) -> transition -> transition
    5.10 +  val skip_proof_open: transition -> transition
    5.11 +  val skip_proof_close: transition -> transition
    5.12    val exec_id: Document_ID.exec -> transition -> transition
    5.13    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    5.14    val add_hook: (transition -> state -> state -> unit) -> unit
    5.15 @@ -510,16 +511,24 @@
    5.16  val proofs = proofs' o K;
    5.17  val proof = proof' o K;
    5.18  
    5.19 +
    5.20 +(* skipped proofs *)
    5.21 +
    5.22  fun actual_proof f = transaction (fn _ =>
    5.23    (fn Proof (prf, x) => Proof (f prf, x)
    5.24      | _ => raise UNDEF));
    5.25  
    5.26  fun skip_proof f = transaction (fn _ =>
    5.27 -  (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
    5.28 +  (fn skip as Skipped_Proof _ => (f (); skip)
    5.29      | _ => raise UNDEF));
    5.30  
    5.31 -fun skip_proof_to_theory pred = transaction (fn _ =>
    5.32 -  (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
    5.33 +val skip_proof_open = transaction (fn _ =>
    5.34 +  (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x)
    5.35 +    | _ => raise UNDEF));
    5.36 +
    5.37 +val skip_proof_close = transaction (fn _ =>
    5.38 +  (fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
    5.39 +    | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x)
    5.40      | _ => raise UNDEF));
    5.41  
    5.42