# HG changeset patch
# User wenzelm
# Date 1538390495 -7200
# Node ID d44cb8a3e5e0a578183155719b09e33dbe1d1da9
# Parent  dabe59286c79d1d013718b5e496683ad3321aae0
HOL-SPARK .prv files are no longer written to the file-system;

diff -r dabe59286c79 -r d44cb8a3e5e0 NEWS
--- a/NEWS	Mon Oct 01 12:19:55 2018 +0200
+++ b/NEWS	Mon Oct 01 12:41:35 2018 +0200
@@ -47,6 +47,12 @@
 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
 provers, has been updated.
 
+* Session HOL-SPARK: .prv files are no longer written to the
+file-system, but exported to the session database. Results may be
+retrieved with the "isabelle export" command-line tool like this:
+
+  isabelle export -x "*:**.prv" HOL-SPARK-Examples
+
 
 *** ML ***
 
diff -r dabe59286c79 -r d44cb8a3e5e0 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/ROOT	Mon Oct 01 12:41:35 2018 +0200
@@ -857,7 +857,6 @@
     SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
-  options [spark_prv = false]
   theories
     "Gcd/Greatest_Common_Divisor"
     "Liseq/Longest_Increasing_Subsequence"
@@ -873,7 +872,7 @@
     "Sqrt/Sqrt"
 
 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
-  options [show_question_marks = false, spark_prv = false]
+  options [show_question_marks = false]
   sessions
     "HOL-SPARK-Examples"
   theories
diff -r dabe59286c79 -r d44cb8a3e5e0 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Oct 01 12:41:35 2018 +0200
@@ -13,13 +13,13 @@
     val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
       {lines = fdl_lines, pos = fdl_pos, ...},
       {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
-    val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
+    val path = fst (Path.split_ext src_path);
   in
     SPARK_VCs.set_vcs
       (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
       (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines))
       (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines)))
-      base prfx thy'
+      path prfx thy'
   end;
 
 fun add_proof_fun_cmd pf thy =
diff -r dabe59286c79 -r d44cb8a3e5e0 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Oct 01 12:19:55 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Oct 01 12:41:35 2018 +0200
@@ -973,11 +973,9 @@
              \because their proofs contain oracles:" proved'));
           val prv_path = Path.ext "prv" path;
           val _ =
-            if File.exists prv_path orelse Options.default_bool \<^system_option>\<open>spark_prv\<close> then
-              File.write prv_path
-               (implode (map (fn (s, _) => snd (strip_number s) ^
-                  " -- proved by " ^ Distribution.version ^ "\n") proved''))
-            else ();
+            Export.export thy (Path.implode prv_path)
+              [implode (map (fn (s, _) => snd (strip_number s) ^
+                " -- proved by " ^ Distribution.version ^ "\n") proved'')];
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
   |> Sign.parent_path;
 
diff -r dabe59286c79 -r d44cb8a3e5e0 src/HOL/SPARK/etc/options
--- a/src/HOL/SPARK/etc/options	Mon Oct 01 12:19:55 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* :mode=isabelle-options: *)
-
-section "HOL-SPARK"
-
-option spark_prv : bool = true
-  -- "produce proof review file after 'spark_end'"