clarified document preparation vs. skip_proofs;
authorwenzelm
Thu Dec 07 19:36:48 2017 +0100 (4 months ago)
changeset 67157d0657c8b7616
parent 67155 9e5b05d54f9d
child 67158 a14b83897c90
clarified document preparation vs. skip_proofs;
NEWS
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/NEWS	Thu Dec 07 15:48:50 2017 +0100
     1.2 +++ b/NEWS	Thu Dec 07 19:36:48 2017 +0100
     1.3 @@ -83,6 +83,9 @@
     1.4  antiquotations in control symbol notation, e.g. \<^const_name> becomes
     1.5  \isactrlconstUNDERSCOREname.
     1.6  
     1.7 +* Document preparation with skip_proofs option now preserves the content
     1.8 +more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
     2.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 07 15:48:50 2017 +0100
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 07 19:36:48 2017 +0100
     2.3 @@ -106,6 +106,8 @@
     2.4    val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     2.5      (string * string list) list list -> context -> state
     2.6    val global_qed: Method.text_range option * bool -> state -> context
     2.7 +  val schematic_goal: state -> bool
     2.8 +  val is_relevant: state -> bool
     2.9    val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    2.10    val local_default_proof: state -> state
    2.11    val local_immediate_proof: state -> state
    2.12 @@ -138,8 +140,6 @@
    2.13      (binding * string option * mixfix) list ->
    2.14      (Attrib.binding * (string * string list) list) list ->
    2.15      (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
    2.16 -  val schematic_goal: state -> bool
    2.17 -  val is_relevant: state -> bool
    2.18    val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
    2.19    val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    2.20    val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
    2.21 @@ -1125,6 +1125,19 @@
    2.22    global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
    2.23  
    2.24  
    2.25 +(* relevant proof states *)
    2.26 +
    2.27 +fun schematic_goal state =
    2.28 +  let val (_, {statement = (_, _, prop), ...}) = find_goal state
    2.29 +  in Goal.is_schematic prop end;
    2.30 +
    2.31 +fun is_relevant state =
    2.32 +  (case try find_goal state of
    2.33 +    NONE => true
    2.34 +  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
    2.35 +      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    2.36 +
    2.37 +
    2.38  (* terminal proof steps *)
    2.39  
    2.40  local
    2.41 @@ -1136,11 +1149,15 @@
    2.42      val initial' = apfst check_closure initial;
    2.43      val terminal' = (apfst o Option.map o apfst) check_closure terminal;
    2.44    in
    2.45 -    state
    2.46 -    |> proof (SOME initial')
    2.47 -    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
    2.48 -    |> Seq.the_result ""
    2.49 -  end;
    2.50 +    if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
    2.51 +      state
    2.52 +      |> proof (SOME (Method.sorry_text false, #2 initial'))
    2.53 +      |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
    2.54 +    else
    2.55 +      state
    2.56 +      |> proof (SOME initial')
    2.57 +      |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
    2.58 +  end |> Seq.the_result "";
    2.59  
    2.60  in
    2.61  
    2.62 @@ -1232,19 +1249,6 @@
    2.63  
    2.64  (** future proofs **)
    2.65  
    2.66 -(* relevant proof states *)
    2.67 -
    2.68 -fun schematic_goal state =
    2.69 -  let val (_, {statement = (_, _, prop), ...}) = find_goal state
    2.70 -  in Goal.is_schematic prop end;
    2.71 -
    2.72 -fun is_relevant state =
    2.73 -  (case try find_goal state of
    2.74 -    NONE => true
    2.75 -  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
    2.76 -      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    2.77 -
    2.78 -
    2.79  (* full proofs *)
    2.80  
    2.81  local
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Dec 07 15:48:50 2017 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Dec 07 19:36:48 2017 +0100
     3.3 @@ -455,7 +455,8 @@
     3.4    (fn Theory (gthy, _) =>
     3.5      let
     3.6        val (finish, prf) = init int gthy;
     3.7 -      val skip = Goal.skip_proofs_enabled ();
     3.8 +      val document = Options.default_string "document";
     3.9 +      val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
    3.10        val schematic_goal = try Proof.schematic_goal prf;
    3.11        val _ =
    3.12          if skip andalso schematic_goal = SOME true then