# HG changeset patch # User wenzelm # Date 1354551539 -3600 # Node ID 6d5dcfb628692773932e8b4b1206dc7760b6ef98 # Parent dddcaeb92e112908e253b81a9409c9c7c6e4947c# Parent 6be9e490d82a05cf28889f1b3f2437b4eda60e8c merged diff -r dddcaeb92e11 -r 6d5dcfb62869 src/HOL/SMT.thy --- 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 = "" ]] diff -r dddcaeb92e11 -r 6d5dcfb62869 src/HOL/Tools/SMT/smt_config.ML --- 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 diff -r dddcaeb92e11 -r 6d5dcfb62869 src/Pure/Isar/proof.ML --- 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; diff -r dddcaeb92e11 -r 6d5dcfb62869 src/Tools/cache_io.ML --- 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 diff -r dddcaeb92e11 -r 6d5dcfb62869 src/Tools/jEdit/src/jEdit.props --- 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