# HG changeset patch
# User wenzelm
# Date 1427286707 -3600
# Node ID e749a0f2f401f3c377893e350a1b3dc1e3aaa0f0
# Parent  87641097d0f369ebd97cb9664a0faac52f860731
HOL-SPARK .prv files are subject to system option spark_prv;
tuned;

diff -r 87641097d0f3 -r e749a0f2f401 etc/components
--- a/etc/components	Wed Mar 25 11:39:52 2015 +0100
+++ b/etc/components	Wed Mar 25 13:31:47 2015 +0100
@@ -4,6 +4,7 @@
 src/HOL/Mirabelle
 src/HOL/Mutabelle
 src/HOL/Library/Sum_of_Squares
+src/HOL/SPARK
 src/HOL/Tools
 src/HOL/Tools/ATP
 src/HOL/TPTP
diff -r 87641097d0f3 -r e749a0f2f401 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 25 11:39:52 2015 +0100
+++ b/src/HOL/ROOT	Wed Mar 25 13:31:47 2015 +0100
@@ -824,7 +824,7 @@
   theories SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
-  options [document = false]
+  options [document = false, spark_prv = false]
   theories
     "Gcd/Greatest_Common_Divisor"
 
@@ -877,7 +877,7 @@
     "RIPEMD-160/rmd/s_r.siv"
 
 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
-  options [show_question_marks = false]
+  options [show_question_marks = false, spark_prv = false]
   theories
     Example_Verification
     VC_Principles
diff -r 87641097d0f3 -r e749a0f2f401 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 25 11:39:52 2015 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 25 13:31:47 2015 +0100
@@ -953,29 +953,33 @@
   | x => x);
 
 fun close incomplete thy =
-  thy |>
-  VCs.map (fn
-      {pfuns, type_map, env = SOME {vcs, path, ...}} =>
+  thy |> VCs.map (fn {pfuns, type_map, env} =>
+    (case env of
+      NONE => error "No SPARK environment is currently open"
+    | SOME {vcs, path, ...} =>
         let
           val (proved, unproved) = partition_vcs vcs;
           val _ = Thm.join_proofs (maps (#2 o snd) proved);
-          val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
-            exists (#oracle o Thm.peek_status) thms) proved
-        in
-          (if null unproved then ()
-           else (if incomplete then warning else error)
-             (Pretty.string_of (pp_open_vcs unproved));
-           if null proved' then ()
-           else warning (Pretty.string_of (pp_vcs
+          val (proved', proved'') =
+            List.partition (fn (_, (_, thms, _, _)) =>
+              exists (#oracle o Thm.peek_status) thms) proved;
+          val _ =
+            if null unproved then ()
+            else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved));
+          val _ =
+            if null proved' then ()
+            else warning (Pretty.string_of (pp_vcs
              "The following VCs are not marked as proved \
              \because their proofs contain oracles:" proved'));
-           File.write (Path.ext "prv" path)
-             (implode (map (fn (s, _) => snd (strip_number s) ^
-                " -- proved by " ^ Distribution.version ^ "\n") proved''));
-           {pfuns = pfuns, type_map = type_map, env = NONE})
-        end
-    | _ => error "No SPARK environment is currently open") |>
-  Sign.parent_path;
+          val prv_path = Path.ext "prv" path;
+          val _ =
+            if File.exists prv_path orelse Options.default_bool @{system_option spark_prv} then
+              File.write prv_path
+               (implode (map (fn (s, _) => snd (strip_number s) ^
+                  " -- proved by " ^ Distribution.version ^ "\n") proved''))
+            else ();
+        in {pfuns = pfuns, type_map = type_map, env = NONE} end))
+  |> Sign.parent_path;
 
 
 (** set up verification conditions **)
diff -r 87641097d0f3 -r e749a0f2f401 src/HOL/SPARK/etc/options
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/etc/options	Wed Mar 25 13:31:47 2015 +0100
@@ -0,0 +1,6 @@
+(* :mode=isabelle-options: *)
+
+section "HOL-SPARK"
+
+option spark_prv : bool = true
+  -- "produce proof review file after 'spark_end'"