# HG changeset patch
# User wenzelm
# Date 1512673508 -3600
# Node ID a14b83897c903824a9330142efcd9339e4aa1210
# Parent  3a9966b88a5082f9be25d39f0d290312d2510774# Parent  d0657c8b7616c7bb9fde476c58a3bca44a5ba460
merged

diff -r 3a9966b88a50 -r a14b83897c90 NEWS
--- a/NEWS	Thu Dec 07 18:04:52 2017 +0100
+++ b/NEWS	Thu Dec 07 20:05:08 2017 +0100
@@ -83,6 +83,9 @@
 antiquotations in control symbol notation, e.g. \<^const_name> becomes
 \isactrlconstUNDERSCOREname.
 
+* Document preparation with skip_proofs option now preserves the content
+more accurately: only terminal proof steps ('by' etc.) are skipped.
+
 
 *** HOL ***
 
diff -r 3a9966b88a50 -r a14b83897c90 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 07 18:04:52 2017 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Dec 07 20:05:08 2017 +0100
@@ -106,6 +106,8 @@
   val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
   val global_qed: Method.text_range option * bool -> state -> context
+  val schematic_goal: state -> bool
+  val is_relevant: state -> bool
   val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   val local_default_proof: state -> state
   val local_immediate_proof: state -> state
@@ -138,8 +140,6 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
-  val schematic_goal: state -> bool
-  val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
   val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
@@ -1125,6 +1125,19 @@
   global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
 
 
+(* relevant proof states *)
+
+fun schematic_goal state =
+  let val (_, {statement = (_, _, prop), ...}) = find_goal state
+  in Goal.is_schematic prop end;
+
+fun is_relevant state =
+  (case try find_goal state of
+    NONE => true
+  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
+      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+
+
 (* terminal proof steps *)
 
 local
@@ -1136,11 +1149,15 @@
     val initial' = apfst check_closure initial;
     val terminal' = (apfst o Option.map o apfst) check_closure terminal;
   in
-    state
-    |> proof (SOME initial')
-    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
-    |> Seq.the_result ""
-  end;
+    if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
+      state
+      |> proof (SOME (Method.sorry_text false, #2 initial'))
+      |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
+    else
+      state
+      |> proof (SOME initial')
+      |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
+  end |> Seq.the_result "";
 
 in
 
@@ -1232,19 +1249,6 @@
 
 (** future proofs **)
 
-(* relevant proof states *)
-
-fun schematic_goal state =
-  let val (_, {statement = (_, _, prop), ...}) = find_goal state
-  in Goal.is_schematic prop end;
-
-fun is_relevant state =
-  (case try find_goal state of
-    NONE => true
-  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
-      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
-
-
 (* full proofs *)
 
 local
diff -r 3a9966b88a50 -r a14b83897c90 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 07 18:04:52 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 07 20:05:08 2017 +0100
@@ -455,7 +455,8 @@
   (fn Theory (gthy, _) =>
     let
       val (finish, prf) = init int gthy;
-      val skip = Goal.skip_proofs_enabled ();
+      val document = Options.default_string "document";
+      val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
       val schematic_goal = try Proof.schematic_goal prf;
       val _ =
         if skip andalso schematic_goal = SOME true then