# HG changeset patch
# User wenzelm
# Date 1320594113 -3600
# Node ID 157e74588c49cccbafd56d231d929859502695fe
# Parent  4849133d7a7862d45306ebb47fff5fa90decfd07
write changed .prv files only, to avoid writing into src file-space by default;

diff -r 4849133d7a78 -r 157e74588c49 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 06 16:29:22 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun Nov 06 16:41:53 2011 +0100
@@ -880,6 +880,10 @@
          prefix = prefix}}
   | x => x);
 
+fun write_prv path s =
+  let val path_prv = Path.ext "prv" path;
+  in if try File.read path_prv = SOME s then () else File.write path_prv s end;
+
 fun close thy =
   thy |>
   VCs.map (fn
@@ -888,7 +892,7 @@
              (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
            (proved, []) =>
              (Thm.join_proofs (maps (the o #2 o snd) proved);
-              File.write (Path.ext "prv" path)
+              write_prv path
                 (implode (map (fn (s, _) => snd (strip_number s) ^
                    " -- proved by " ^ Distribution.version ^ "\n") proved));
               {pfuns = pfuns, type_map = type_map, env = NONE})