# HG changeset patch # User wenzelm # Date 1285172508 -7200 # Node ID 8052101883c310cd04934a51aaa831e93cdb0219 # Parent b926f8ec9cacaa3f5b07626b79596cfc946cdfc7 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning; diff -r b926f8ec9cac -r 8052101883c3 NEWS --- a/NEWS Wed Sep 22 17:46:59 2010 +0200 +++ b/NEWS Wed Sep 22 18:21:48 2010 +0200 @@ -244,6 +244,9 @@ *** ML *** +* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its +meaning. + * Renamed structure PureThy to Pure_Thy and moved most of its operations to structure Global_Theory, to emphasize that this is rarely-used global-only stuff. diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Import/HOL/ROOT.ML --- a/src/HOL/Import/HOL/ROOT.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Import/HOL/ROOT.ML Wed Sep 22 18:21:48 2010 +0200 @@ -1,2 +1,2 @@ use_thy "~~/src/HOL/Old_Number_Theory/Primes"; -setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"]; +Unsynchronized.setmp quick_and_dirty true use_thys ["HOL4Prob", "HOL4"]; diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Induct/ROOT.ML Wed Sep 22 18:21:48 2010 +0200 @@ -1,4 +1,4 @@ -setmp_noncritical quick_and_dirty true +Unsynchronized.setmp quick_and_dirty true use_thys ["Common_Patterns"]; use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList", diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Nitpick_Examples/ROOT.ML --- a/src/HOL/Nitpick_Examples/ROOT.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Nitpick_Examples/ROOT.ML Wed Sep 22 18:21:48 2010 +0200 @@ -5,4 +5,4 @@ Nitpick examples. *) -setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"]; +Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"]; diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Nominal/Examples/ROOT.ML --- a/src/HOL/Nominal/Examples/ROOT.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Wed Sep 22 18:21:48 2010 +0200 @@ -1,3 +1,3 @@ use_thys ["Nominal_Examples"]; -setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; +Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"]; diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Sep 22 18:21:48 2010 +0200 @@ -1,5 +1,20 @@ -use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"]; +use_thys [ + "Predicate_Compile_Examples", + "Predicate_Compile_Quickcheck_Examples", + "Specialisation_Examples", + "IMP_1", + "IMP_2", + "IMP_3", + "IMP_4"]; + if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then - (warning "No prolog system found - could not use example theories that require a prolog system"; ()) + (warning "No prolog system found - skipping some example theories"; ()) else - (use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"]; setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"]) + (use_thys [ + "Code_Prolog_Examples", + "Context_Free_Grammar_Example", + "Hotel_Example", + "Lambda_Example", + "List_Examples"]; + Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]); + diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/HOL/Tools/try.ML Wed Sep 22 18:21:48 2010 +0200 @@ -18,7 +18,7 @@ val _ = ProofGeneralPgip.add_preference Preferences.category_tracing - (setmp_noncritical auto true (fn () => + (Unsynchronized.setmp auto true (fn () => Preferences.bool_pref auto "auto-try" "Try standard proof methods.") ()); diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/Isar/proof.ML Wed Sep 22 18:21:48 2010 +0200 @@ -976,7 +976,7 @@ else (); val test_proof = try (local_skip_proof true) - |> setmp_noncritical testing true + |> Unsynchronized.setmp testing true |> Exn.capture; fun after_qed' results = diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/multithreading.ML --- a/src/Pure/ML-Systems/multithreading.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/multithreading.ML Wed Sep 22 18:21:48 2010 +0200 @@ -14,7 +14,7 @@ sig include BASIC_MULTITHREADING val available: bool - val max_threads: int Unsynchronized.ref + val max_threads: int ref val max_threads_value: unit -> int val enabled: unit -> bool val no_interrupts: Thread.threadAttribute list @@ -24,7 +24,7 @@ val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a val sync_wait: Thread.threadAttribute list option -> Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result - val trace: int Unsynchronized.ref + val trace: int ref val tracing: int -> (unit -> string) -> unit val tracing_time: bool -> Time.time -> (unit -> string) -> unit val real_time: ('a -> unit) -> 'a -> Time.time @@ -38,7 +38,7 @@ (* options *) val available = false; -val max_threads = Unsynchronized.ref (1: int); +val max_threads = ref (1: int); fun max_threads_value () = 1: int; fun enabled () = false; @@ -57,7 +57,7 @@ (* tracing *) -val trace = Unsynchronized.ref (0: int); +val trace = ref (0: int); fun tracing _ _ = (); fun tracing_time _ _ _ = (); fun real_time f x = (f x; Time.zeroTime); @@ -72,7 +72,7 @@ (* serial numbers *) -local val count = Unsynchronized.ref (0: int) +local val count = ref (0: int) in fun serial () = (count := ! count + 1; ! count) end; end; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Sep 22 18:21:48 2010 +0200 @@ -31,7 +31,7 @@ val available = true; -val max_threads = Unsynchronized.ref 0; +val max_threads = ref 0; fun max_threads_value () = let val m = ! max_threads in @@ -109,7 +109,7 @@ (* tracing *) -val trace = Unsynchronized.ref 0; +val trace = ref 0; fun tracing level msg = if level > ! trace then () @@ -143,7 +143,7 @@ fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () => let val worker = Thread.self (); - val timeout = Unsynchronized.ref false; + val timeout = ref false; val watchdog = Thread.fork (fn () => (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []); @@ -168,7 +168,7 @@ (*result state*) datatype result = Wait | Signal | Result of int; - val result = Unsynchronized.ref Wait; + val result = ref Wait; val lock = Mutex.mutex (); val cond = ConditionVar.conditionVar (); fun set_result res = @@ -226,8 +226,8 @@ local val critical_lock = Mutex.mutex (); -val critical_thread = Unsynchronized.ref (NONE: Thread.thread option); -val critical_name = Unsynchronized.ref ""; +val critical_thread = ref (NONE: Thread.thread option); +val critical_name = ref ""; in @@ -269,7 +269,7 @@ local val serial_lock = Mutex.mutex (); -val serial_count = Unsynchronized.ref 0; +val serial_count = ref 0; in diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml-5.2.1.ML --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Sep 22 18:21:48 2010 +0200 @@ -3,8 +3,6 @@ Compatibility wrapper for Poly/ML 5.2.1. *) -use "ML-Systems/unsynchronized.ML"; - open Thread; structure ML_Name_Space = @@ -18,6 +16,10 @@ use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; +use "ML-Systems/unsynchronized.ML"; + +val _ = PolyML.Compiler.forgetValue "ref"; +val _ = PolyML.Compiler.forgetType "ref"; val pointer_eq = PolyML.pointerEq; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml-5.2.ML --- a/src/Pure/ML-Systems/polyml-5.2.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/polyml-5.2.ML Wed Sep 22 18:21:48 2010 +0200 @@ -3,8 +3,6 @@ Compatibility wrapper for Poly/ML 5.2. *) -use "ML-Systems/unsynchronized.ML"; - open Thread; structure ML_Name_Space = @@ -17,9 +15,12 @@ fun reraise exn = raise exn; use "ML-Systems/polyml_common.ML"; - use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; +use "ML-Systems/unsynchronized.ML"; + +val _ = PolyML.Compiler.forgetValue "ref"; +val _ = PolyML.Compiler.forgetType "ref"; val pointer_eq = PolyML.pointerEq; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Wed Sep 22 18:21:48 2010 +0200 @@ -3,8 +3,6 @@ Compatibility wrapper for Poly/ML 5.3 and 5.4. *) -use "ML-Systems/unsynchronized.ML"; - open Thread; structure ML_Name_Space = @@ -21,6 +19,10 @@ use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; +use "ML-Systems/unsynchronized.ML"; + +val _ = PolyML.Compiler.forgetValue "ref"; +val _ = PolyML.Compiler.forgetType "ref"; val pointer_eq = PolyML.pointerEq; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Wed Sep 22 18:21:48 2010 +0200 @@ -29,8 +29,6 @@ val _ = PolyML.Compiler.forgetValue "foldl"; val _ = PolyML.Compiler.forgetValue "foldr"; val _ = PolyML.Compiler.forgetValue "print"; -val _ = PolyML.Compiler.forgetValue "ref"; -val _ = PolyML.Compiler.forgetType "ref"; (* Compiler options *) @@ -62,7 +60,7 @@ (* toplevel printing *) local - val depth = Unsynchronized.ref 10; + val depth = ref 10; in fun get_print_depth () = ! depth; fun print_depth n = (depth := n; PolyML.print_depth n); diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Sep 22 18:21:48 2010 +0200 @@ -7,7 +7,6 @@ fun reraise exn = raise exn; use "ML-Systems/proper_int.ML"; -use "ML-Systems/unsynchronized.ML"; use "ML-Systems/overloading_smlnj.ML"; use "General/exn.ML"; use "ML-Systems/single_assignment.ML"; @@ -159,6 +158,9 @@ end; +use "ML-Systems/unsynchronized.ML"; + + (** OS related **) diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/thread_dummy.ML --- a/src/Pure/ML-Systems/thread_dummy.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/thread_dummy.ML Wed Sep 22 18:21:48 2010 +0200 @@ -60,7 +60,7 @@ local -val data = Unsynchronized.ref ([]: Universal.universal Unsynchronized.ref list); +val data = ref ([]: Universal.universal ref list); fun find_data tag = let @@ -75,7 +75,7 @@ fun setLocal (tag, x) = (case find_data tag of SOME r => r := Universal.tagInject tag x - | NONE => data := Unsynchronized.ref (Universal.tagInject tag x) :: ! data); + | NONE => data := ref (Universal.tagInject tag x) :: ! data); end; end; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/unsynchronized.ML --- a/src/Pure/ML-Systems/unsynchronized.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ML-Systems/unsynchronized.ML Wed Sep 22 18:21:48 2010 +0200 @@ -18,4 +18,13 @@ fun inc i = (i := ! i + (1: int); ! i); fun dec i = (i := ! i - (1: int); ! i); +fun setmp flag value f x = + uninterruptible (fn restore_attributes => fn () => + let + val orig_value = ! flag; + val _ = flag := value; + val result = Exn.capture (restore_attributes f) x; + val _ = flag := orig_value; + in Exn.release result end) (); + end; diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Wed Sep 22 18:21:48 2010 +0200 @@ -78,7 +78,7 @@ (* preferences of Pure *) -val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () => +val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => let fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); @@ -164,7 +164,7 @@ thm_deps_pref]; val proof_preferences = - [setmp_noncritical quick_and_dirty true (fn () => + [Unsynchronized.setmp quick_and_dirty true (fn () => bool_pref quick_and_dirty "quick-and-dirty" "Take a few short cuts") (), diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 22 18:21:48 2010 +0200 @@ -1044,7 +1044,7 @@ This works for preferences but not generally guaranteed because we haven't done full setup here (e.g., no pgml mode) *) fun process_pgip_emacs str = - setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str + Unsynchronized.setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str end diff -r b926f8ec9cac -r 8052101883c3 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/System/session.ML Wed Sep 22 18:21:48 2010 +0200 @@ -110,11 +110,11 @@ in () end else use root; finish ())) - |> setmp_noncritical Proofterm.proofs level - |> setmp_noncritical print_mode (modes @ print_mode_value ()) - |> setmp_noncritical Goal.parallel_proofs parallel_proofs - |> setmp_noncritical Multithreading.trace trace_threads - |> setmp_noncritical Multithreading.max_threads + |> Unsynchronized.setmp Proofterm.proofs level + |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) + |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs + |> Unsynchronized.setmp Multithreading.trace trace_threads + |> Unsynchronized.setmp Multithreading.max_threads (if Multithreading.available then max_threads else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/Thy/html.ML Wed Sep 22 18:21:48 2010 +0200 @@ -277,7 +277,7 @@ (* document *) val charset = Unsynchronized.ref "ISO-8859-1"; -fun with_charset s = setmp_noncritical charset s; (* FIXME unreliable *) +fun with_charset s = Unsynchronized.setmp charset s; (* FIXME unreliable *) fun begin_document title = let val cs = ! charset in diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/Thy/present.ML Wed Sep 22 18:21:48 2010 +0200 @@ -165,7 +165,7 @@ CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f)); val suppress_tex_source = Unsynchronized.ref false; -fun no_document f x = setmp_noncritical suppress_tex_source true f x; +fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; (* FIXME unreliable *) fun init_theory_info name info = change_browser_info (fn (theories, files, tex_index, html_index, graph) => diff -r b926f8ec9cac -r 8052101883c3 src/Pure/library.ML --- a/src/Pure/library.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Pure/library.ML Wed Sep 22 18:21:48 2010 +0200 @@ -56,7 +56,6 @@ val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool val exists: ('a -> bool) -> 'a list -> bool val forall: ('a -> bool) -> 'a list -> bool - val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c @@ -306,18 +305,8 @@ (* flags *) -(*temporarily set flag during execution*) -fun setmp_noncritical flag value f x = - uninterruptible (fn restore_attributes => fn () => - let - val orig_value = ! flag; - val _ = flag := value; - val result = Exn.capture (restore_attributes f) x; - val _ = flag := orig_value; - in Exn.release result end) (); - fun setmp_CRITICAL flag value f x = - NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x); + NAMED_CRITICAL "setmp" (fn () => Unsynchronized.setmp flag value f x); fun setmp_thread_data tag orig_data data f x = uninterruptible (fn restore_attributes => fn () => diff -r b926f8ec9cac -r 8052101883c3 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Tools/auto_solve.ML Wed Sep 22 18:21:48 2010 +0200 @@ -25,7 +25,7 @@ val _ = ProofGeneralPgip.add_preference Preferences.category_tracing - (setmp_noncritical auto true (fn () => + (Unsynchronized.setmp auto true (fn () => Preferences.bool_pref auto "auto-solve" "Try to solve conjectures with existing theorems.") ()); diff -r b926f8ec9cac -r 8052101883c3 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Sep 22 17:46:59 2010 +0200 +++ b/src/Tools/quickcheck.ML Wed Sep 22 18:21:48 2010 +0200 @@ -42,7 +42,7 @@ val _ = ProofGeneralPgip.add_preference Preferences.category_tracing - (setmp_noncritical auto true (fn () => + (Unsynchronized.setmp auto true (fn () => Preferences.bool_pref auto "auto-quickcheck" "Run Quickcheck automatically.") ());