merged

--- a/src/HOL/SMT.thy	Mon Dec 03 13:24:55 2012 +0100
+++ b/src/HOL/SMT.thy	Mon Dec 03 17:18:59 2012 +0100
@@ -256,6 +256,8 @@
 The filename should be given as an explicit path.  It is good
 practice to use the name of the current theory (with ending
 @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
+Certificate files should be used at most once in a certain theory context,
+to avoid race conditions with other concurrent accesses.
 *}
 
 declare [[ smt_certificates = "" ]]

--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 03 13:24:55 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 03 17:18:59 2012 +0100
@@ -202,7 +202,7 @@
   else
     Path.explode name
     |> Path.append (Thy_Load.master_directory (Context.theory_of context))
-    |> SOME o Cache_IO.make)
+    |> SOME o Cache_IO.unsynchronized_init)
 
 val certificates_of = Certificates.get o Context.Proof
 

--- a/src/Pure/Isar/proof.ML	Mon Dec 03 13:24:55 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Dec 03 17:18:59 2012 +0100
@@ -1059,7 +1059,7 @@
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
     fun fail_msg ctxt =
-      "Local statement will fail to refine any pending goal" ::
+      "Local statement fails to refine any pending goal" ::
       (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
@@ -1072,7 +1072,7 @@
         writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
       else ();
     val test_proof =
-      try (local_skip_proof true)
+      local_skip_proof true
       |> Unsynchronized.setmp testing true
       |> Exn.interruptible_capture;
 
@@ -1085,8 +1085,7 @@
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     |> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
-        Exn.Res (SOME _) => goal_state
-      | Exn.Res NONE => error (fail_msg (context_of goal_state))
+        Exn.Res _ => goal_state
       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 

--- a/src/Tools/cache_io.ML	Mon Dec 03 13:24:55 2012 +0100
+++ b/src/Tools/cache_io.ML	Mon Dec 03 17:18:59 2012 +0100
@@ -11,17 +11,15 @@
     output: string list,
     redirected_output: string list,
     return_code: int}
-  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
-    result
+  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
   type cache
-  val make: Path.T -> cache
+  val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
   val lookup: cache -> string -> result option * string
-  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
-    string -> result
+  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
   val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
 end
 
@@ -42,7 +40,7 @@
     val _ = File.write in_path str
     val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
     val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-  in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+  in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =
   Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
@@ -59,55 +57,54 @@
 
 fun cache_path_of (Cache {path, ...}) = path
 
-fun load cache_path =
+fun unsynchronized_init cache_path =
   let
-    fun err () = error ("Cache IO: corrupted cache file: " ^
-      File.shell_path cache_path)
+    val table =
+      if File.exists cache_path then
+        let
+          fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path)
 
-    fun int_of_string s =
-      (case read_int (raw_explode s) of
-        (i, []) => i
-      | _ => err ())
-
-    fun split line =
-      (case space_explode " " line of
-        [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
-      | _ => err ())
+          fun int_of_string s =
+            (case read_int (raw_explode s) of
+              (i, []) => i
+            | _ => err ())
 
-    fun parse line ((i, l), tab) =
-      if i = l
-      then
-        let val (key, l1, l2) = split line
-        in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
-      else ((i+1, l), tab)
-  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
-
-fun make path =
-  let val table = if File.exists path then load path else (1, Symtab.empty)
-  in Cache {path=path, table=Synchronized.var "Cache_IO" table} end
+          fun split line =
+            (case space_explode " " line of
+              [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
+            | _ => err ())
 
-fun load_cached_result cache_path (p, len1, len2) =
-  let
-    fun load line (i, xsp) =
-      if i < p then (i+1, xsp)
-      else if i < p + len1 then (i+1, apfst (cons line) xsp)
-      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
-      else (i, xsp)
-    val (out, err) =
-      pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
-  in {output=err, redirected_output=out, return_code=0} end
+          fun parse line ((i, l), tab) =
+            if i = l
+            then
+              let val (key, l1, l2) = split line
+              in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
+            else ((i+1, l), tab)
+        in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
+      else (1, Symtab.empty)
+  in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
 
-fun lookup (Cache {path=cache_path, table}) str =
+fun lookup (Cache {path = cache_path, table}) str =
   let val key = SHA1.rep (SHA1.digest str)
   in
-    (case Symtab.lookup (snd (Synchronized.value table)) key of
-      NONE => (NONE, key)
-    | SOME pos => (SOME (load_cached_result cache_path pos), key))
+    Synchronized.change_result table (fn tab =>
+      (case Symtab.lookup (snd tab) key of
+        NONE => ((NONE, key), tab)
+      | SOME (p, len1, len2) =>
+          let
+            fun load line (i, xsp) =
+              if i < p then (i+1, xsp)
+              else if i < p + len1 then (i+1, apfst (cons line) xsp)
+              else if i < p + len2 then (i+1, apsnd (cons line) xsp)
+              else (i, xsp)
+            val (out, err) =
+              pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
+          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end
 
-fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
+fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
   let
-    val {output=err, redirected_output=out, return_code} = run make_cmd str
+    val {output = err, redirected_output=out, return_code} = run make_cmd str
     val (l1, l2) = pairself length (out, err)
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
     val lines = map (suffix "\n") (header :: out @ err)
@@ -117,7 +114,7 @@
       else
         let val _ = File.append_list cache_path lines
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
-  in {output=err, redirected_output=out, return_code=return_code} end
+  in {output = err, redirected_output = out, return_code = return_code} end
 
 fun run_cached cache make_cmd str =
   (case lookup cache str of

--- a/src/Tools/jEdit/src/jEdit.props	Mon Dec 03 13:24:55 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Dec 03 17:18:59 2012 +0100
@@ -214,6 +214,7 @@
 sidekick.complete-popup.accept-characters=\\n\\t
 sidekick.complete-popup.insert-characters=
 sidekick.splitter.location=721
+systrayicon=false
 tip.show=false
 twoStageSave=false
 vfs.browser.dock-position=floating