--- a/src/Pure/Concurrent/future.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Sep 29 11:49:22 2009 +0200
@@ -99,13 +99,13 @@
(* global state *)
-val queue = ref Task_Queue.empty;
-val next = ref 0;
-val workers = ref ([]: (Thread.thread * bool) list);
-val scheduler = ref (NONE: Thread.thread option);
-val excessive = ref 0;
-val canceled = ref ([]: Task_Queue.group list);
-val do_shutdown = ref false;
+val queue = Unsynchronized.ref Task_Queue.empty;
+val next = Unsynchronized.ref 0;
+val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list);
+val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
+val excessive = Unsynchronized.ref 0;
+val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val do_shutdown = Unsynchronized.ref false;
(* synchronization *)
@@ -162,7 +162,8 @@
in (result, job) end;
fun do_cancel group = (*requires SYNCHRONIZED*)
- (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
+ (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
+ broadcast scheduler_event);
fun execute name (task, group, jobs) =
let
@@ -171,7 +172,7 @@
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "finish" (fn () =>
let
- val maximal = change_result queue (Task_Queue.finish task);
+ val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
val _ =
if ok then ()
else if Task_Queue.cancel (! queue) group then ()
@@ -188,7 +189,8 @@
fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
fun change_active active = (*requires SYNCHRONIZED*)
- change workers (AList.update Thread.equal (Thread.self (), active));
+ Unsynchronized.change workers
+ (AList.update Thread.equal (Thread.self (), active));
(* worker threads *)
@@ -198,14 +200,15 @@
fun worker_next () = (*requires SYNCHRONIZED*)
if ! excessive > 0 then
- (dec excessive;
- change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
+ (Unsynchronized.dec excessive;
+ Unsynchronized.change workers
+ (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
broadcast scheduler_event;
NONE)
else if count_active () > Multithreading.max_threads_value () then
(worker_wait scheduler_event; worker_next ())
else
- (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
+ (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
NONE => (worker_wait work_available; worker_next ())
| some => some);
@@ -215,13 +218,13 @@
| SOME work => (execute name work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
- change workers (cons (SimpleThread.fork false (fn () =>
+ Unsynchronized.change workers (cons (SimpleThread.fork false (fn () =>
(broadcast scheduler_event; worker_loop name)), true));
(* scheduler *)
-val last_status = ref Time.zeroTime;
+val last_status = Unsynchronized.ref Time.zeroTime;
val next_status = Time.fromMilliseconds 500;
val next_round = Time.fromMilliseconds 50;
@@ -263,7 +266,8 @@
val _ = excessive := l - mm;
val _ =
if mm > l then
- funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
+ funpow (mm - l) (fn () =>
+ worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) ()
else ();
(*canceled groups*)
@@ -272,7 +276,7 @@
else
(Multithreading.tracing 1 (fn () =>
string_of_int (length (! canceled)) ^ " canceled groups");
- change canceled (filter_out (Task_Queue.cancel (! queue)));
+ Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue)));
broadcast_work ());
(*delay loop*)
@@ -317,7 +321,8 @@
val (result, job) = future_job group e;
val task = SYNCHRONIZED "enqueue" (fn () =>
let
- val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
+ val (task, minimal) =
+ Unsynchronized.change_result queue (Task_Queue.enqueue group deps pri job);
val _ = if minimal then signal work_available else ();
val _ = scheduler_check ();
in task end);
@@ -347,7 +352,7 @@
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
else
- (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
+ (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
(NONE, []) => NONE
| (NONE, deps') => (worker_wait work_finished; join_next deps')
| (SOME work, deps') => SOME (work, deps'));
--- a/src/Pure/Concurrent/synchronized.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Tue Sep 29 11:49:22 2009 +0200
@@ -24,13 +24,13 @@
{name: string,
lock: Mutex.mutex,
cond: ConditionVar.conditionVar,
- var: 'a ref};
+ var: 'a Unsynchronized.ref};
fun var name x = Var
{name = name,
lock = Mutex.mutex (),
cond = ConditionVar.conditionVar (),
- var = ref x};
+ var = Unsynchronized.ref x};
fun value (Var {var, ...}) = ! var;
--- a/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 11:49:22 2009 +0200
@@ -7,9 +7,9 @@
structure Synchronized: SYNCHRONIZED =
struct
-datatype 'a var = Var of 'a ref;
+datatype 'a var = Var of 'a Unsynchronized.ref;
-fun var _ x = Var (ref x);
+fun var _ x = Var (Unsynchronized.ref x);
fun value (Var var) = ! var;
fun timed_access (Var var) _ f =
--- a/src/Pure/General/file.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/file.ML Tue Sep 29 11:49:22 2009 +0200
@@ -85,7 +85,8 @@
(* file identification *)
local
- val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
+ val ident_cache =
+ Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
in
fun check_cache (path, time) = CRITICAL (fn () =>
@@ -94,7 +95,8 @@
| SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
- change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
+ Unsynchronized.change ident_cache
+ (Symtab.update (path, {time_stamp = time, id = id})));
end;
--- a/src/Pure/General/lazy.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/lazy.ML Tue Sep 29 11:49:22 2009 +0200
@@ -26,12 +26,12 @@
Lazy of unit -> 'a |
Result of 'a Exn.result;
-type 'a lazy = 'a T ref;
+type 'a lazy = 'a T Unsynchronized.ref;
fun same (r1: 'a lazy, r2) = r1 = r2;
-fun lazy e = ref (Lazy e);
-fun value x = ref (Result (Exn.Result x));
+fun lazy e = Unsynchronized.ref (Lazy e);
+fun value x = Unsynchronized.ref (Result (Exn.Result x));
fun peek r =
(case ! r of
--- a/src/Pure/General/markup.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/markup.ML Tue Sep 29 11:49:22 2009 +0200
@@ -323,10 +323,10 @@
local
val default = {output = default_output};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name output = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {output = output})));
+ Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
--- a/src/Pure/General/name_space.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/name_space.ML Tue Sep 29 11:49:22 2009 +0200
@@ -9,9 +9,9 @@
signature BASIC_NAME_SPACE =
sig
- val long_names: bool ref
- val short_names: bool ref
- val unique_names: bool ref
+ val long_names: bool Unsynchronized.ref
+ val short_names: bool Unsynchronized.ref
+ val unique_names: bool Unsynchronized.ref
end;
signature NAME_SPACE =
@@ -105,9 +105,9 @@
else ext (get_accesses space name)
end;
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
+val long_names = Unsynchronized.ref false;
+val short_names = Unsynchronized.ref false;
+val unique_names = Unsynchronized.ref true;
fun extern space name =
extern_flags
@@ -261,6 +261,6 @@
end;
-structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
-open BasicNameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+open Basic_Name_Space;
--- a/src/Pure/General/output.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/output.ML Tue Sep 29 11:49:22 2009 +0200
@@ -11,13 +11,13 @@
val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
- val tolerate_legacy_features: bool ref
+ val tolerate_legacy_features: bool Unsynchronized.ref
val legacy_feature: string -> unit
val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
val timeit: (unit -> 'a) -> 'a
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
- val timing: bool ref
+ val timing: bool Unsynchronized.ref
end;
signature OUTPUT =
@@ -32,18 +32,18 @@
val std_output: output -> unit
val std_error: output -> unit
val writeln_default: output -> unit
- val writeln_fn: (output -> unit) ref
- val priority_fn: (output -> unit) ref
- val tracing_fn: (output -> unit) ref
- val warning_fn: (output -> unit) ref
- val error_fn: (output -> unit) ref
- val debug_fn: (output -> unit) ref
- val prompt_fn: (output -> unit) ref
- val status_fn: (output -> unit) ref
+ val writeln_fn: (output -> unit) Unsynchronized.ref
+ val priority_fn: (output -> unit) Unsynchronized.ref
+ val tracing_fn: (output -> unit) Unsynchronized.ref
+ val warning_fn: (output -> unit) Unsynchronized.ref
+ val error_fn: (output -> unit) Unsynchronized.ref
+ val debug_fn: (output -> unit) Unsynchronized.ref
+ val prompt_fn: (output -> unit) Unsynchronized.ref
+ val status_fn: (output -> unit) Unsynchronized.ref
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
- val debugging: bool ref
+ val debugging: bool Unsynchronized.ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
end;
@@ -60,10 +60,10 @@
local
val default = {output = default_output, escape = default_escape};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name output escape = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {output = output, escape = escape})));
+ Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
@@ -91,14 +91,14 @@
(* Isabelle output channels *)
-val writeln_fn = ref writeln_default;
-val priority_fn = ref (fn s => ! writeln_fn s);
-val tracing_fn = ref (fn s => ! writeln_fn s);
-val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
-val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
-val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
-val prompt_fn = ref std_output;
-val status_fn = ref (fn _: string => ());
+val writeln_fn = Unsynchronized.ref writeln_default;
+val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
+val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
+val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = Unsynchronized.ref std_output;
+val status_fn = Unsynchronized.ref (fn _: string => ());
fun writeln s = ! writeln_fn (output s);
fun priority s = ! priority_fn (output s);
@@ -108,13 +108,13 @@
fun prompt s = ! prompt_fn (output s);
fun status s = ! status_fn (output s);
-val tolerate_legacy_features = ref true;
+val tolerate_legacy_features = Unsynchronized.ref true;
fun legacy_feature s =
(if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
fun no_warnings f = setmp warning_fn (K ()) f;
-val debugging = ref false;
+val debugging = Unsynchronized.ref false;
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
@@ -140,9 +140,9 @@
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
(*global timing mode*)
-val timing = ref false;
+val timing = Unsynchronized.ref false;
end;
-structure BasicOutput: BASIC_OUTPUT = Output;
-open BasicOutput;
+structure Basic_Output: BASIC_OUTPUT = Output;
+open Basic_Output;
--- a/src/Pure/General/pretty.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/pretty.ML Tue Sep 29 11:49:22 2009 +0200
@@ -86,10 +86,10 @@
local
val default = {indent = default_indent};
- val modes = ref (Symtab.make [("", default)]);
+ val modes = Unsynchronized.ref (Symtab.make [("", default)]);
in
fun add_mode name indent = CRITICAL (fn () =>
- change modes (Symtab.update_new (name, {indent = indent})));
+ Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
@@ -186,14 +186,14 @@
breakgain = m div 20, (*minimum added space required of a break*)
emergencypos = m div 2}; (*position too far to right*)
-val margin_info = ref (make_margin_info 76);
+val margin_info = Unsynchronized.ref (make_margin_info 76);
fun setmargin m = margin_info := make_margin_info m;
fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
(* depth limitation *)
-val depth = ref 0; (*maximum depth; 0 means no limit*)
+val depth = Unsynchronized.ref 0; (*maximum depth; 0 means no limit*)
fun setdepth dp = (depth := dp);
local
--- a/src/Pure/General/print_mode.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/print_mode.ML Tue Sep 29 11:49:22 2009 +0200
@@ -7,9 +7,9 @@
signature BASIC_PRINT_MODE =
sig
- val print_mode: string list ref (*global template*)
- val print_mode_value: unit -> string list (*thread-local value*)
- val print_mode_active: string -> bool (*thread-local value*)
+ val print_mode: string list Unsynchronized.ref (*global template*)
+ val print_mode_value: unit -> string list (*thread-local value*)
+ val print_mode_active: string -> bool (*thread-local value*)
end;
signature PRINT_MODE =
@@ -28,7 +28,7 @@
val input = "input";
val internal = "internal";
-val print_mode = ref ([]: string list);
+val print_mode = Unsynchronized.ref ([]: string list);
val tag = Universal.tag () : string list option Universal.tag;
fun print_mode_value () =
--- a/src/Pure/General/secure.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/General/secure.ML Tue Sep 29 11:49:22 2009 +0200
@@ -23,7 +23,7 @@
(** secure flag **)
-val secure = ref false;
+val secure = Unsynchronized.ref false;
fun set_secure () = secure := true;
fun is_secure () = ! secure;
--- a/src/Pure/Isar/code.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/code.ML Tue Sep 29 11:49:22 2009 +0200
@@ -217,8 +217,8 @@
purge: theory -> string list -> Object.T -> Object.T
};
-val kinds = ref (Datatab.empty: kind Datatab.table);
-val kind_keys = ref ([]: serial list);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
+val kind_keys = Unsynchronized.ref ([]: serial list);
fun invoke f k = case Datatab.lookup (! kinds) k
of SOME kind => f kind
@@ -230,8 +230,8 @@
let
val k = serial ();
val kind = {empty = empty, purge = purge};
- val _ = change kinds (Datatab.update (k, kind));
- val _ = change kind_keys (cons k);
+ val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
+ val _ = Unsynchronized.change kind_keys (cons k);
in k end;
fun invoke_init k = invoke (fn kind => #empty kind) k;
@@ -252,13 +252,13 @@
structure Code_Data = TheoryDataFun
(
- type T = spec * data ref;
+ type T = spec * data Unsynchronized.ref;
val empty = (make_spec (false,
- (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
- fun copy (spec, data) = (spec, ref (! data));
+ (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
+ fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
val extend = copy;
fun merge pp ((spec1, data1), (spec2, data2)) =
- (merge_spec (spec1, spec2), ref empty_data);
+ (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
);
fun thy_data f thy = f ((snd o Code_Data.get) thy);
@@ -267,7 +267,7 @@
case Datatab.lookup (! data_ref) kind
of SOME x => x
| NONE => let val y = invoke_init kind
- in (change data_ref (Datatab.update (kind, y)); y) end;
+ in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
in
@@ -281,11 +281,11 @@
| SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
fun map_exec_purge touched f thy =
- Code_Data.map (fn (exec, data) => (f exec, ref (case touched
+ Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
| NONE => empty_data))) thy;
-val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
+val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
@@ -332,7 +332,7 @@
let
val data = get_ensure_init kind data_ref;
val data' = f (dest data);
- in (change data_ref (Datatab.update (kind, mk data')); data') end;
+ in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
in thy_data chnge end;
fun change_yield_data (kind, mk, dest) =
@@ -341,7 +341,7 @@
let
val data = get_ensure_init kind data_ref;
val (x, data') = f (dest data);
- in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
+ in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
in thy_data chnge end;
end; (*local*)
--- a/src/Pure/Isar/isar_document.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML Tue Sep 29 11:49:22 2009 +0200
@@ -112,18 +112,18 @@
(** global configuration **)
local
- val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
- val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
- val global_documents = ref (Symtab.empty: document Symtab.table);
+ val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
+ val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
+ val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
in
-fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
+fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
-fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
+fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
-fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
+fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
fun init () = NAMED_CRITICAL "Isar" (fn () =>
--- a/src/Pure/Isar/local_syntax.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/local_syntax.ML Tue Sep 29 11:49:22 2009 +0200
@@ -4,7 +4,7 @@
Local syntax depending on theory syntax.
*)
-val show_structs = ref false;
+val show_structs = Unsynchronized.ref false;
signature LOCAL_SYNTAX =
sig
--- a/src/Pure/Isar/method.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/method.ML Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
sig
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val trace_rules: bool ref
+ val trace_rules: bool Unsynchronized.ref
end;
signature METHOD =
@@ -215,7 +215,7 @@
(* rule etc. -- single-step refinements *)
-val trace_rules = ref false;
+val trace_rules = Unsynchronized.ref false;
fun trace ctxt rules =
if ! trace_rules andalso not (null rules) then
--- a/src/Pure/Isar/outer_keyword.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_keyword.ML Tue Sep 29 11:49:22 2009 +0200
@@ -116,16 +116,16 @@
local
-val global_commands = ref (Symtab.empty: T Symtab.table);
-val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
+val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
+val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
in
fun get_commands () = CRITICAL (fn () => ! global_commands);
fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
-fun change_commands f = CRITICAL (fn () => change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
+fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
+fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
end;
--- a/src/Pure/Isar/outer_lex.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_lex.ML Tue Sep 29 11:49:22 2009 +0200
@@ -83,7 +83,7 @@
datatype slot =
Slot |
Value of value option |
- Assignable of value option ref;
+ Assignable of value option Unsynchronized.ref;
(* datatype token *)
@@ -245,7 +245,7 @@
(* static binding *)
(*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
| assignable tok = tok;
(*2nd stage: assign values as side-effect of scanning*)
@@ -253,7 +253,7 @@
| assign _ _ = ();
(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
| closure tok = tok;
--- a/src/Pure/Isar/outer_syntax.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Sep 29 11:49:22 2009 +0200
@@ -88,11 +88,11 @@
local
-val global_commands = ref (Symtab.empty: command Symtab.table);
-val global_markups = ref ([]: (string * ThyOutput.markup) list);
+val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
+val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
fun change_commands f = CRITICAL (fn () =>
- (change global_commands f;
+ (Unsynchronized.change global_commands f;
global_markups :=
Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
(! global_commands) []));
--- a/src/Pure/Isar/proof.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/proof.ML Tue Sep 29 11:49:22 2009 +0200
@@ -30,8 +30,8 @@
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
val get_goal: state -> context * (thm list * thm)
- val show_main_goal: bool ref
- val verbose: bool ref
+ val show_main_goal: bool Unsynchronized.ref
+ val verbose: bool Unsynchronized.ref
val pretty_state: int -> state -> Pretty.T list
val pretty_goals: bool -> state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
@@ -315,7 +315,7 @@
(** pretty_state **)
-val show_main_goal = ref false;
+val show_main_goal = Unsynchronized.ref false;
val verbose = ProofContext.verbose;
fun pretty_facts _ _ NONE = []
@@ -930,8 +930,8 @@
fun gen_show prep_att prepp before_qed after_qed stmt int state =
let
- val testing = ref false;
- val rule = ref (NONE: thm option);
+ 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" ::
(case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
--- a/src/Pure/Isar/proof_context.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 29 11:49:22 2009 +0200
@@ -123,15 +123,15 @@
val add_abbrev: string -> Properties.T ->
binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
- val verbose: bool ref
+ val verbose: bool Unsynchronized.ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
val print_binds: Proof.context -> unit
val print_lthms: Proof.context -> unit
val print_cases: Proof.context -> unit
- val debug: bool ref
- val prems_limit: int ref
+ val debug: bool Unsynchronized.ref
+ val prems_limit: int Unsynchronized.ref
val pretty_ctxt: Proof.context -> Pretty.T list
val pretty_context: Proof.context -> Pretty.T list
val query_type: Proof.context -> string -> Properties.T
@@ -1208,9 +1208,9 @@
(** print context information **)
-val debug = ref false;
+val debug = Unsynchronized.ref false;
-val verbose = ref false;
+val verbose = Unsynchronized.ref false;
fun verb f x = if ! verbose then f (x ()) else [];
fun setmp_verbose f x = Library.setmp verbose true f x;
@@ -1320,7 +1320,7 @@
(* core context *)
-val prems_limit = ref ~1;
+val prems_limit = Unsynchronized.ref ~1;
fun pretty_ctxt ctxt =
if ! prems_limit < 0 andalso not (! debug) then []
--- a/src/Pure/Isar/toplevel.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Sep 29 11:49:22 2009 +0200
@@ -24,12 +24,12 @@
val enter_proof_body: state -> Proof.state
val print_state_context: state -> unit
val print_state: bool -> state -> unit
- val quiet: bool ref
- val debug: bool ref
- val interact: bool ref
- val timing: bool ref
- val profiling: int ref
- val skip_proofs: bool ref
+ val quiet: bool Unsynchronized.ref
+ val debug: bool Unsynchronized.ref
+ val interact: bool Unsynchronized.ref
+ val timing: bool Unsynchronized.ref
+ val profiling: int Unsynchronized.ref
+ val skip_proofs: bool Unsynchronized.ref
exception TERMINATE
exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
@@ -216,12 +216,12 @@
(** toplevel transitions **)
-val quiet = ref false;
+val quiet = Unsynchronized.ref false;
val debug = Output.debugging;
-val interact = ref false;
+val interact = Unsynchronized.ref false;
val timing = Output.timing;
-val profiling = ref 0;
-val skip_proofs = ref false;
+val profiling = Unsynchronized.ref 0;
+val skip_proofs = Unsynchronized.ref false;
exception TERMINATE = Runtime.TERMINATE;
exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
@@ -550,9 +550,9 @@
(* post-transition hooks *)
-local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
+local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
-fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun get_hooks () = CRITICAL (fn () => ! hooks);
end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 11:49:22 2009 +0200
@@ -5,11 +5,11 @@
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
let
- val in_buffer = ref (explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val in_buffer = Unsynchronized.ref (explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
- val current_line = ref line;
+ val current_line = Unsynchronized.ref line;
fun get () =
(case ! in_buffer of
[] => ""
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 11:49:22 2009 +0200
@@ -14,9 +14,9 @@
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val current_line = Unsynchronized.ref start_line;
+ val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 11:49:22 2009 +0200
@@ -14,9 +14,9 @@
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
- val line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
+ val line = Unsynchronized.ref start_line;
+ val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 11:49:22 2009 +0200
@@ -31,7 +31,7 @@
val available = true;
-val max_threads = ref 0;
+val max_threads = Unsynchronized.ref 0;
val tested_platform =
let val ml_platform = getenv "ML_PLATFORM"
@@ -114,7 +114,7 @@
(* tracing *)
-val trace = ref 0;
+val trace = Unsynchronized.ref 0;
fun tracing level msg =
if level > ! trace then ()
@@ -148,7 +148,7 @@
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
let
val worker = Thread.self ();
- val timeout = ref false;
+ val timeout = Unsynchronized.ref false;
val watchdog = Thread.fork (fn () =>
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
@@ -173,7 +173,7 @@
(*result state*)
datatype result = Wait | Signal | Result of int;
- val result = ref Wait;
+ val result = Unsynchronized.ref Wait;
val lock = Mutex.mutex ();
val cond = ConditionVar.conditionVar ();
fun set_result res =
@@ -231,8 +231,8 @@
local
val critical_lock = Mutex.mutex ();
-val critical_thread = ref (NONE: Thread.thread option);
-val critical_name = ref "";
+val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
+val critical_name = Unsynchronized.ref "";
in
@@ -274,7 +274,7 @@
local
val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
+val serial_count = Unsynchronized.ref 0;
in
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 11:49:22 2009 +0200
@@ -91,8 +91,8 @@
if null toks then Position.none
else ML_Lex.end_pos_of (List.last toks);
- val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
- val line = ref (the_default 1 (Position.line_of pos));
+ val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+ val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
fun get () =
@@ -106,9 +106,9 @@
(* output *)
- val output_buffer = ref Buffer.empty;
+ val output_buffer = Unsynchronized.ref Buffer.empty;
fun output () = Buffer.content (! output_buffer);
- fun put s = change output_buffer (Buffer.add s);
+ fun put s = Unsynchronized.change output_buffer (Buffer.add s);
fun put_message {message, hard, location, context = _} =
(put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
--- a/src/Pure/ML/ml_context.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML/ml_context.ML Tue Sep 29 11:49:22 2009 +0200
@@ -19,20 +19,21 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val stored_thms: thm list ref
+ val stored_thms: thm list Unsynchronized.ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
type antiq =
{struct_name: string, background: Proof.context} ->
(Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: bool -> Position.T -> Symbol_Pos.text -> unit
val eval_file: Path.T -> unit
val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
- val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
+ val evaluate: Proof.context -> bool ->
+ string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
end
@@ -53,7 +54,7 @@
(* theorem bindings *)
-val stored_thms: thm list ref = ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
fun ml_store sel (name, ths) =
let
@@ -89,12 +90,13 @@
local
-val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
+val global_parsers =
+ Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
in
fun add_antiq name scan = CRITICAL (fn () =>
- change global_parsers (fn tab =>
+ Unsynchronized.change global_parsers (fn tab =>
(if not (Symtab.defined tab name) then ()
else warning ("Redefined ML antiquotation: " ^ quote name);
Symtab.update (name, scan) tab)));
@@ -162,7 +164,7 @@
in (ml, SOME (Context.Proof ctxt')) end;
in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun eval verbose pos txt =
let
--- a/src/Pure/Proof/extraction.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Sep 29 11:49:22 2009 +0200
@@ -91,7 +91,7 @@
Pattern.rewrite_term thy [] (condrew' :: procs) tm
and condrew' tm =
let
- val cache = ref ([] : (term * term) list);
+ val cache = Unsynchronized.ref ([] : (term * term) list);
fun lookup f x = (case AList.lookup (op =) (!cache) x of
NONE =>
let val y = f x
--- a/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
signature RECONSTRUCT =
sig
- val quiet_mode : bool ref
+ val quiet_mode : bool Unsynchronized.ref
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
@@ -19,7 +19,7 @@
open Proofterm;
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
fun vars_of t = map Var (rev (Term.add_vars t []));
--- a/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 11:49:22 2009 +0200
@@ -18,11 +18,11 @@
get: unit -> string,
set: string -> unit}
val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
- 'a ref -> string -> string -> preference
- val string_pref: string ref -> string -> string -> preference
- val int_pref: int ref -> string -> string -> preference
- val nat_pref: int ref -> string -> string -> preference
- val bool_pref: bool ref -> string -> string -> preference
+ 'a Unsynchronized.ref -> string -> string -> preference
+ val string_pref: string Unsynchronized.ref -> string -> string -> preference
+ val int_pref: int Unsynchronized.ref -> string -> string -> preference
+ val nat_pref: int Unsynchronized.ref -> string -> string -> preference
+ val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
type T = (string * preference list) list
val pure_preferences: T
val remove: string -> T -> T
@@ -95,8 +95,9 @@
let
fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
fun set s =
- if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN)
- else change print_mode (remove (op =) thm_depsN);
+ if PgipTypes.read_pgipbool s
+ then Unsynchronized.change print_mode (insert (op =) thm_depsN)
+ else Unsynchronized.change print_mode (remove (op =) thm_depsN);
in
mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
"Track theorem dependencies within Proof General"
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 11:49:22 2009 +0200
@@ -226,7 +226,7 @@
(* init *)
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
@@ -239,9 +239,9 @@
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_thy_loader ();
setup_present_hook ();
- set initialized);
+ Unsynchronized.set initialized);
sync_thy_loader ();
- change print_mode (update (op =) proof_generalN);
+ Unsynchronized.change print_mode (update (op =) proof_generalN);
Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 11:49:22 2009 +0200
@@ -32,20 +32,20 @@
(** print mode **)
val proof_generalN = "ProofGeneral";
-val pgmlsymbols_flag = ref true;
+val pgmlsymbols_flag = Unsynchronized.ref true;
(* assembling and issuing PGIP packets *)
-val pgip_refid = ref NONE: string option ref;
-val pgip_refseq = ref NONE: int option ref;
+val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
+val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
local
val pgip_class = "pg"
val pgip_tag = "Isabelle/Isar"
- val pgip_id = ref ""
- val pgip_seq = ref 0
- fun pgip_serial () = inc pgip_seq
+ val pgip_id = Unsynchronized.ref ""
+ val pgip_seq = Unsynchronized.ref 0
+ fun pgip_serial () = Unsynchronized.inc pgip_seq
fun assemble_pgips pgips =
Pgip { tag = SOME pgip_tag,
@@ -65,7 +65,7 @@
fun matching_pgip_id id = (id = ! pgip_id)
-val output_xml_fn = ref Output.writeln_default
+val output_xml_fn = Unsynchronized.ref Output.writeln_default
fun output_xml s = ! output_xml_fn (XML.string_of s);
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -280,7 +280,7 @@
(* theorem dependeny output *)
-val show_theorem_dependencies = ref false;
+val show_theorem_dependencies = Unsynchronized.ref false;
local
@@ -368,13 +368,13 @@
(* Preferences: tweak for PGIP interfaces *)
-val preferences = ref Preferences.pure_preferences;
+val preferences = Unsynchronized.ref Preferences.pure_preferences;
fun add_preference cat pref =
- CRITICAL (fn () => change preferences (Preferences.add cat pref));
+ CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
fun setup_preferences_tweak () =
- CRITICAL (fn () => change preferences
+ CRITICAL (fn () => Unsynchronized.change preferences
(Preferences.set_default ("show-question-marks", "false") #>
Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
Preferences.remove "theorem-dependencies" #> (* set internally *)
@@ -471,7 +471,7 @@
fun set_proverflag_pgmlsymbols b =
(pgmlsymbols_flag := b;
NAMED_CRITICAL "print_mode" (fn () =>
- change print_mode
+ Unsynchronized.change print_mode
(fn mode =>
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
@@ -677,7 +677,7 @@
about this special status, but for now we just keep a local reference.
*)
-val currently_open_file = ref (NONE : pgipurl option)
+val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
fun get_currently_open_file () = ! currently_open_file;
@@ -779,7 +779,7 @@
*)
local
- val current_working_dir = ref (NONE : string option)
+ val current_working_dir = Unsynchronized.ref (NONE : string option)
in
fun changecwd_dir newdirpath =
let
@@ -1021,7 +1021,7 @@
(* init *)
-val initialized = ref false;
+val initialized = Unsynchronized.ref false;
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
@@ -1035,9 +1035,9 @@
setup_present_hook ();
init_pgip_session_id ();
welcome ();
- set initialized);
+ Unsynchronized.set initialized);
sync_thy_loader ();
- change print_mode (update (op =) proof_generalN);
+ Unsynchronized.change print_mode (update (op =) proof_generalN);
pgip_toplevel tty_src);
@@ -1045,7 +1045,7 @@
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
local
- val pgip_output_channel = ref Output.writeln_default
+ val pgip_output_channel = Unsynchronized.ref Output.writeln_default
in
(* Set recipient for PGIP results *)
--- a/src/Pure/ROOT.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ROOT.ML Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
end;
(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = ref false;
+val quick_and_dirty = Unsynchronized.ref false;
print_depth 10;
--- a/src/Pure/Syntax/ast.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/ast.ML Tue Sep 29 11:49:22 2009 +0200
@@ -24,8 +24,8 @@
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
val unfold_ast_p: string -> ast -> ast list * ast
- val trace_ast: bool ref
- val stat_ast: bool ref
+ val trace_ast: bool Unsynchronized.ref
+ val stat_ast: bool Unsynchronized.ref
end;
signature AST =
@@ -173,9 +173,9 @@
fun normalize trace stat get_rules pre_ast =
let
- val passes = ref 0;
- val failed_matches = ref 0;
- val changes = ref 0;
+ val passes = Unsynchronized.ref 0;
+ val failed_matches = Unsynchronized.ref 0;
+ val changes = Unsynchronized.ref 0;
fun subst _ (ast as Constant _) = ast
| subst env (Variable x) = the (Symtab.lookup env x)
@@ -184,8 +184,8 @@
fun try_rules ((lhs, rhs) :: pats) ast =
(case match ast lhs of
SOME (env, args) =>
- (inc changes; SOME (mk_appl (subst env rhs) args))
- | NONE => (inc failed_matches; try_rules pats ast))
+ (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
+ | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
| try_rules [] _ = NONE;
val try_headless_rules = try_rules (get_rules "");
@@ -226,7 +226,7 @@
val old_changes = ! changes;
val new_ast = norm ast;
in
- inc passes;
+ Unsynchronized.inc passes;
if old_changes = ! changes then new_ast else normal new_ast
end;
@@ -245,8 +245,8 @@
(* normalize_ast *)
-val trace_ast = ref false;
-val stat_ast = ref false;
+val trace_ast = Unsynchronized.ref false;
+val stat_ast = Unsynchronized.ref false;
fun normalize_ast get_rules ast =
normalize (! trace_ast) (! stat_ast) get_rules ast;
--- a/src/Pure/Syntax/parser.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Sep 29 11:49:22 2009 +0200
@@ -17,7 +17,7 @@
Tip of Lexicon.token
val parse: gram -> string -> Lexicon.token list -> parsetree list
val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
- val branching_level: int ref
+ val branching_level: int Unsynchronized.ref
end;
structure Parser: PARSER =
@@ -690,7 +690,7 @@
else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
-val branching_level = ref 600; (*trigger value for warnings*)
+val branching_level = Unsynchronized.ref 600; (*trigger value for warnings*)
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
@@ -821,7 +821,7 @@
val Estate = Array.array (s, []);
in
Array.update (Estate, 0, S0);
- get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
+ get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
end;
--- a/src/Pure/Syntax/printer.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/printer.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,11 +6,11 @@
signature PRINTER0 =
sig
- val show_brackets: bool ref
- val show_sorts: bool ref
- val show_types: bool ref
- val show_no_free_types: bool ref
- val show_all_types: bool ref
+ val show_brackets: bool Unsynchronized.ref
+ val show_sorts: bool Unsynchronized.ref
+ val show_types: bool Unsynchronized.ref
+ val show_no_free_types: bool Unsynchronized.ref
+ val show_all_types: bool Unsynchronized.ref
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
@@ -42,11 +42,11 @@
(** options for printing **)
-val show_types = ref false;
-val show_sorts = ref false;
-val show_brackets = ref false;
-val show_no_free_types = ref false;
-val show_all_types = ref false;
+val show_types = Unsynchronized.ref false;
+val show_sorts = Unsynchronized.ref false;
+val show_brackets = Unsynchronized.ref false;
+val show_no_free_types = Unsynchronized.ref false;
+val show_all_types = Unsynchronized.ref false;
fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
--- a/src/Pure/Syntax/syn_trans.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
signature SYN_TRANS0 =
sig
- val eta_contract: bool ref
+ val eta_contract: bool Unsynchronized.ref
val atomic_abs_tr': string * typ * term -> term * term
val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
@@ -276,7 +276,7 @@
(*do (partial) eta-contraction before printing*)
-val eta_contract = ref true;
+val eta_contract = Unsynchronized.ref true;
fun eta_contr tm =
let
--- a/src/Pure/Syntax/syntax.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Sep 29 11:49:22 2009 +0200
@@ -36,9 +36,9 @@
val print_syntax: syntax -> unit
val guess_infix: syntax -> string -> mixfix option
val read_token: string -> Symbol_Pos.T list * Position.T
- val ambiguity_is_error: bool ref
- val ambiguity_level: int ref
- val ambiguity_limit: int ref
+ val ambiguity_is_error: bool Unsynchronized.ref
+ val ambiguity_level: int Unsynchronized.ref
+ val ambiguity_limit: int Unsynchronized.ref
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
(string -> bool * string) -> (string -> string option) ->
@@ -472,9 +472,9 @@
(* read_ast *)
-val ambiguity_is_error = ref false;
-val ambiguity_level = ref 1;
-val ambiguity_limit = ref 10;
+val ambiguity_is_error = Unsynchronized.ref false;
+val ambiguity_level = Unsynchronized.ref 1;
+val ambiguity_limit = Unsynchronized.ref 10;
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
@@ -711,7 +711,7 @@
unparse_typ: Proof.context -> typ -> Pretty.T,
unparse_term: Proof.context -> term -> Pretty.T};
- val operations = ref (NONE: operations option);
+ val operations = Unsynchronized.ref (NONE: operations option);
fun operation which ctxt x =
(case ! operations of
--- a/src/Pure/System/isabelle_process.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Sep 29 11:49:22 2009 +0200
@@ -130,7 +130,7 @@
(* init *)
fun init out =
- (change print_mode (update (op =) isabelle_processN);
+ (Unsynchronized.change print_mode (update (op =) isabelle_processN);
setup_channels out |> init_message;
OuterKeyword.report ();
Output.status (Markup.markup Markup.ready "");
--- a/src/Pure/System/isar.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/isar.ML Tue Sep 29 11:49:22 2009 +0200
@@ -18,7 +18,7 @@
val undo: int -> unit
val kill: unit -> unit
val kill_proof: unit -> unit
- val crashes: exn list ref
+ val crashes: exn list Unsynchronized.ref
val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
val loop: unit -> unit
val main: unit -> unit
@@ -36,9 +36,9 @@
(*previous state, state transition -- regular commands only*)
local
- val global_history = ref ([]: history);
- val global_state = ref Toplevel.toplevel;
- val global_exn = ref (NONE: (exn * string) option);
+ val global_history = Unsynchronized.ref ([]: history);
+ val global_state = Unsynchronized.ref Toplevel.toplevel;
+ val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
in
fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
@@ -115,7 +115,7 @@
(* toplevel loop *)
-val crashes = ref ([]: exn list);
+val crashes = Unsynchronized.ref ([]: exn list);
local
@@ -130,7 +130,7 @@
handle exn =>
(Output.error_msg (ML_Compiler.exn_message exn)
handle crash =>
- (CRITICAL (fn () => change crashes (cons crash));
+ (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
raw_loop secure src)
end;
--- a/src/Pure/System/session.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/System/session.ML Tue Sep 29 11:49:22 2009 +0200
@@ -21,10 +21,10 @@
(* session state *)
-val session = ref ([Context.PureN]: string list);
-val session_path = ref ([]: string list);
-val session_finished = ref false;
-val remote_path = ref (NONE: Url.T option);
+val session = Unsynchronized.ref ([Context.PureN]: string list);
+val session_path = Unsynchronized.ref ([]: string list);
+val session_finished = Unsynchronized.ref false;
+val remote_path = Unsynchronized.ref (NONE: Url.T option);
(* access path *)
--- a/src/Pure/Thy/html.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/html.ML Tue Sep 29 11:49:22 2009 +0200
@@ -267,8 +267,8 @@
(* document *)
-val charset = ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;
+val charset = Unsynchronized.ref "ISO-8859-1";
+fun with_charset s = setmp_noncritical charset s; (* FIXME *)
fun begin_document title =
let val cs = ! charset in
--- a/src/Pure/Thy/present.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/present.ML Tue Sep 29 11:49:22 2009 +0200
@@ -161,10 +161,11 @@
(* state *)
-val browser_info = ref empty_browser_info;
-fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
+val browser_info = Unsynchronized.ref empty_browser_info;
+fun change_browser_info f =
+ CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
-val suppress_tex_source = ref false;
+val suppress_tex_source = Unsynchronized.ref false;
fun no_document f x = setmp_noncritical suppress_tex_source true f x;
fun init_theory_info name info =
@@ -229,7 +230,7 @@
(* state *)
-val session_info = ref (NONE: session_info option);
+val session_info = Unsynchronized.ref (NONE: session_info option);
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
@@ -534,5 +535,5 @@
end;
-structure BasicPresent: BASIC_PRESENT = Present;
-open BasicPresent;
+structure Basic_Present: BASIC_PRESENT = Present;
+open Basic_Present;
--- a/src/Pure/Thy/thy_info.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Sep 29 11:49:22 2009 +0200
@@ -50,9 +50,9 @@
val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
local
- val hooks = ref ([]: (action -> string -> unit) list);
+ val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
in
- fun add_hook f = CRITICAL (fn () => change hooks (cons f));
+ fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
end;
@@ -111,10 +111,10 @@
type thy = deps option * theory option;
local
- val database = ref (Graph.empty: thy Graph.T);
+ val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
in
fun get_thys () = ! database;
- fun change_thys f = CRITICAL (fn () => Library.change database f);
+ fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
end;
--- a/src/Pure/Thy/thy_load.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML Tue Sep 29 11:49:22 2009 +0200
@@ -37,14 +37,16 @@
(* maintain load path *)
-local val load_path = ref [Path.current] in
+local val load_path = Unsynchronized.ref [Path.current] in
fun show_path () = map Path.implode (! load_path);
-fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
-fun path_add s =
- CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
+fun del_path s = CRITICAL (fn () =>
+ Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun add_path s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun path_add s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
fun reset_path () = load_path := [Path.current];
fun with_paths ss f x =
@@ -124,5 +126,5 @@
end;
-structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
-open BasicThyLoad;
+structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
+open Basic_Thy_Load;
--- a/src/Pure/Thy/thy_output.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,11 +6,11 @@
signature THY_OUTPUT =
sig
- val display: bool ref
- val quotes: bool ref
- val indent: int ref
- val source: bool ref
- val break: bool ref
+ val display: bool Unsynchronized.ref
+ val quotes: bool Unsynchronized.ref
+ val indent: int Unsynchronized.ref
+ val source: bool Unsynchronized.ref
+ val break: bool Unsynchronized.ref
val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
val defined_command: string -> bool
@@ -21,7 +21,7 @@
val antiquotation: string -> 'a context_parser ->
({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
- val modes: string list ref
+ val modes: string list Unsynchronized.ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
@@ -42,11 +42,11 @@
(** global options **)
-val display = ref false;
-val quotes = ref false;
-val indent = ref 0;
-val source = ref false;
-val break = ref false;
+val display = Unsynchronized.ref false;
+val quotes = Unsynchronized.ref false;
+val indent = Unsynchronized.ref 0;
+val source = Unsynchronized.ref false;
+val break = Unsynchronized.ref false;
@@ -55,10 +55,10 @@
local
val global_commands =
- ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
+ Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
val global_options =
- ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
+ Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
fun add_item kind (name, x) tab =
(if not (Symtab.defined tab name) then ()
@@ -67,8 +67,10 @@
in
-fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
-fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
+fun add_commands xs =
+ CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
+fun add_options xs =
+ CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
fun defined_command name = Symtab.defined (! global_commands) name;
fun defined_option name = Symtab.defined (! global_options) name;
@@ -143,7 +145,7 @@
(* eval_antiquote *)
-val modes = ref ([]: string list);
+val modes = Unsynchronized.ref ([]: string list);
fun eval_antiquote lex state (txt, pos) =
let
--- a/src/Pure/Tools/find_theorems.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Sep 29 11:49:22 2009 +0200
@@ -9,8 +9,8 @@
datatype 'term criterion =
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
Pattern of 'term
- val tac_limit: int ref
- val limit: int ref
+ val tac_limit: int Unsynchronized.ref
+ val limit: int Unsynchronized.ref
val find_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
@@ -186,7 +186,7 @@
end
else NONE
-val tac_limit = ref 5;
+val tac_limit = Unsynchronized.ref 5;
fun filter_solves ctxt goal =
let
@@ -372,7 +372,7 @@
(Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
Facts.dest_static [] (ProofContext.facts_of ctxt));
-val limit = ref 40;
+val limit = Unsynchronized.ref 40;
fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/codegen.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/codegen.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,10 +6,10 @@
signature CODEGEN =
sig
- val quiet_mode : bool ref
+ val quiet_mode : bool Unsynchronized.ref
val message : string -> unit
- val mode : string list ref
- val margin : int ref
+ val mode : string list Unsynchronized.ref
+ val margin : int Unsynchronized.ref
val string_of : Pretty.T -> string
val str : string -> Pretty.T
@@ -75,9 +75,9 @@
val mk_type: bool -> typ -> Pretty.T
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
- val test_fn: (int -> term list option) ref
+ val test_fn: (int -> term list option) Unsynchronized.ref
val test_term: Proof.context -> term -> int -> term list option
- val eval_result: (unit -> term) ref
+ val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -102,12 +102,12 @@
structure Codegen : CODEGEN =
struct
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
-val mode = ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list);
-val margin = ref 80;
+val margin = Unsynchronized.ref 80;
fun string_of p = (Pretty.string_of |>
PrintMode.setmp [] |>
@@ -878,7 +878,8 @@
[mk_gen gr module true xs a T, mk_type true T]) Ts) @
(if member (op =) xs s then [str a] else []))));
-val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
+val test_fn : (int -> term list option) Unsynchronized.ref =
+ Unsynchronized.ref (fn _ => NONE);
fun test_term ctxt t =
let
@@ -912,7 +913,7 @@
(**** Evaluator for terms ****)
-val eval_result = ref (fn () => Bound 0);
+val eval_result = Unsynchronized.ref (fn () => Bound 0);
fun eval_term thy t =
let
--- a/src/Pure/context.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/context.ML Tue Sep 29 11:49:22 2009 +0200
@@ -107,7 +107,7 @@
extend: Object.T -> Object.T,
merge: Pretty.pp -> Object.T * Object.T -> Object.T};
-val kinds = ref (Datatab.empty: kind Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
fun invoke f k =
(case Datatab.lookup (! kinds) k of
@@ -125,7 +125,7 @@
let
val k = serial ();
val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
- val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
+ val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
in k end;
val copy_data = Datatab.map' invoke_copy;
@@ -149,7 +149,7 @@
datatype theory =
Theory of
(*identity*)
- {self: theory ref option, (*dynamic self reference -- follows theory changes*)
+ {self: theory Unsynchronized.ref option, (*dynamic self reference -- follows theory changes*)
draft: bool, (*draft mode -- linear destructive changes*)
id: serial, (*identifier*)
ids: unit Inttab.table} * (*cumulative identifiers of non-drafts -- symbolic body content*)
@@ -186,14 +186,15 @@
fun eq_id (i: int, j) = i = j;
fun is_stale
- (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
+ (Theory ({self =
+ SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
not (eq_id (id, id'))
| is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
| vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
let
- val r = ref thy;
+ val r = Unsynchronized.ref thy;
val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
in r := thy'; thy' end;
@@ -243,9 +244,9 @@
theory in external data structures -- a plain theory value would
become stale as the self reference moves on*)
-datatype theory_ref = TheoryRef of theory ref;
+datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
-fun deref (TheoryRef (ref thy)) = thy;
+fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
fun check_thy thy = (*thread-safe version*)
let val thy_ref = TheoryRef (the_self thy) in
@@ -437,7 +438,7 @@
local
-val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
fun invoke_init k =
(case Datatab.lookup (! kinds) k of
@@ -470,7 +471,7 @@
fun declare init =
let
val k = serial ();
- val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
+ val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
in k end;
fun get k dest prf =
--- a/src/Pure/display.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/display.ML Tue Sep 29 11:49:22 2009 +0200
@@ -7,10 +7,10 @@
signature BASIC_DISPLAY =
sig
- val goals_limit: int ref
- val show_consts: bool ref
- val show_hyps: bool ref
- val show_tags: bool ref
+ val goals_limit: int Unsynchronized.ref
+ val show_consts: bool Unsynchronized.ref
+ val show_hyps: bool Unsynchronized.ref
+ val show_tags: bool Unsynchronized.ref
end;
signature DISPLAY =
@@ -39,8 +39,8 @@
val goals_limit = Goal_Display.goals_limit;
val show_consts = Goal_Display.show_consts;
-val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
-val show_tags = ref false; (*false: suppress tags*)
+val show_hyps = Unsynchronized.ref false; (*false: print meta-hypotheses as dots*)
+val show_tags = Unsynchronized.ref false; (*false: suppress tags*)
--- a/src/Pure/goal.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/goal.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
signature BASIC_GOAL =
sig
- val parallel_proofs: int ref
+ val parallel_proofs: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -102,7 +102,7 @@
(* future_enabled *)
-val parallel_proofs = ref 1;
+val parallel_proofs = Unsynchronized.ref 1;
fun future_enabled () =
Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
--- a/src/Pure/goal_display.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/goal_display.ML Tue Sep 29 11:49:22 2009 +0200
@@ -7,8 +7,8 @@
signature GOAL_DISPLAY =
sig
- val goals_limit: int ref
- val show_consts: bool ref
+ val goals_limit: int Unsynchronized.ref
+ val show_consts: bool Unsynchronized.ref
val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
thm -> Pretty.T list
@@ -18,8 +18,8 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit = ref 10; (*max number of goals to print*)
-val show_consts = ref false; (*true: show consts with types in proof state output*)
+val goals_limit = Unsynchronized.ref 10; (*max number of goals to print*)
+val show_consts = Unsynchronized.ref false; (*true: show consts with types in proof state output*)
fun pretty_flexpair ctxt (t, u) = Pretty.block
[Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
--- a/src/Pure/meta_simplifier.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Sep 29 11:49:22 2009 +0200
@@ -11,9 +11,9 @@
signature BASIC_META_SIMPLIFIER =
sig
- val debug_simp: bool ref
- val trace_simp: bool ref
- val trace_simp_depth_limit: int ref
+ val debug_simp: bool Unsynchronized.ref
+ val trace_simp: bool Unsynchronized.ref
+ val trace_simp_depth_limit: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
type simpset
@@ -84,7 +84,7 @@
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
- depth: int * bool ref,
+ depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
{congs: (string * thm) list * string list,
procs: proc Net.net,
@@ -112,7 +112,7 @@
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
val theory_context: theory -> simpset -> simpset
- val debug_bounds: bool ref
+ val debug_bounds: bool Unsynchronized.ref
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
val set_solvers: solver list -> simpset -> simpset
val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
@@ -190,7 +190,7 @@
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
- depth: int * bool ref,
+ depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
{congs: (string * thm) list * string list,
procs: proc Net.net,
@@ -256,7 +256,7 @@
val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
val simp_depth_limit = Config.int simp_depth_limit_value;
-val trace_simp_depth_limit = ref 1;
+val trace_simp_depth_limit = Unsynchronized.ref 1;
fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
if depth > ! trace_simp_depth_limit then
@@ -266,7 +266,8 @@
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
(rules, prems, bounds,
- (depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
+ (depth + 1,
+ if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
@@ -275,8 +276,8 @@
exception SIMPLIFIER of string * thm;
-val debug_simp = ref false;
-val trace_simp = ref false;
+val debug_simp = Unsynchronized.ref false;
+val trace_simp = Unsynchronized.ref false;
local
@@ -746,7 +747,7 @@
(* empty *)
fun init_ss mk_rews termless subgoal_tac solvers =
- make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
+ make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
@@ -1209,7 +1210,7 @@
prover: how to solve premises in conditional rewrites and congruences
*)
-val debug_bounds = ref false;
+val debug_bounds = Unsynchronized.ref false;
fun check_bounds ss ct =
if ! debug_bounds then
@@ -1337,5 +1338,5 @@
end;
-structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
-open BasicMetaSimplifier;
+structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
+open Basic_Meta_Simplifier;
--- a/src/Pure/old_goals.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/old_goals.ML Tue Sep 29 11:49:22 2009 +0200
@@ -19,7 +19,7 @@
type proof
val premises: unit -> thm list
val reset_goals: unit -> unit
- val result_error_fn: (thm -> string -> thm) ref
+ val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
val print_sign_exn: theory -> exn -> 'a
val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
@@ -233,21 +233,21 @@
(*** References ***)
(*Current assumption list -- set by "goal".*)
-val curr_prems = ref([] : thm list);
+val curr_prems = Unsynchronized.ref([] : thm list);
(*Return assumption list -- useful if you didn't save "goal"'s result. *)
fun premises() = !curr_prems;
(*Current result maker -- set by "goal", used by "result". *)
fun init_mkresult _ = error "No goal has been supplied in subgoal module";
-val curr_mkresult = ref (init_mkresult: bool*thm->thm);
+val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
(*List of previous goal stacks, for the undo operation. Set by setstate.
A list of lists!*)
-val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
+val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
(* Stack of proof attempts *)
-val proofstack = ref([]: proof list);
+val proofstack = Unsynchronized.ref([]: proof list);
(*reset all refs*)
fun reset_goals () =
@@ -272,7 +272,7 @@
Goal_Display.pretty_goals_without_context (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
-val result_error_fn = ref result_error_default;
+val result_error_fn = Unsynchronized.ref result_error_default;
(*Common treatment of "goal" and "prove_goal":
--- a/src/Pure/pattern.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/pattern.ML Tue Sep 29 11:49:22 2009 +0200
@@ -14,7 +14,7 @@
signature PATTERN =
sig
- val trace_unify_fail: bool ref
+ val trace_unify_fail: bool Unsynchronized.ref
val aeconv: term * term -> bool
val eta_long: typ list -> term -> term
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -40,7 +40,7 @@
exception Unif;
exception Pattern;
-val trace_unify_fail = ref false;
+val trace_unify_fail = Unsynchronized.ref false;
fun string_of_term thy env binders t =
Syntax.string_of_term_global thy
--- a/src/Pure/proofterm.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/proofterm.ML Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
signature BASIC_PROOFTERM =
sig
- val proofs: int ref
+ val proofs: int Unsynchronized.ref
datatype proof =
MinProof
@@ -885,7 +885,7 @@
(***** axioms and theorems *****)
-val proofs = ref 2;
+val proofs = Unsynchronized.ref 2;
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/search.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/search.ML Tue Sep 29 11:49:22 2009 +0200
@@ -13,23 +13,23 @@
val THEN_MAYBE : tactic * tactic -> tactic
val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
- val trace_DEPTH_FIRST : bool ref
+ val trace_DEPTH_FIRST : bool Unsynchronized.ref
val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
val DEPTH_SOLVE : tactic -> tactic
val DEPTH_SOLVE_1 : tactic -> tactic
val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
- val iter_deepen_limit : int ref
+ val iter_deepen_limit : int Unsynchronized.ref
val has_fewer_prems : int -> thm -> bool
val IF_UNSOLVED : tactic -> tactic
val SOLVE : tactic -> tactic
val DETERM_UNTIL_SOLVED: tactic -> tactic
- val trace_BEST_FIRST : bool ref
+ val trace_BEST_FIRST : bool Unsynchronized.ref
val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
-> tactic
- val trace_ASTAR : bool ref
+ val trace_ASTAR : bool Unsynchronized.ref
val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
-> tactic
@@ -50,7 +50,7 @@
(**** Depth-first search ****)
-val trace_DEPTH_FIRST = ref false;
+val trace_DEPTH_FIRST = Unsynchronized.ref false;
(*Searches until "satp" reports proof tree as satisfied.
Suppresses duplicate solutions to minimize search space.*)
@@ -130,7 +130,7 @@
(*No known example (on 1-5-2007) needs even thirty*)
-val iter_deepen_limit = ref 50;
+val iter_deepen_limit = Unsynchronized.ref 50;
(*Depth-first iterative deepening search for a state that satisfies satp
tactic tac0 sets up the initial goal queue, while tac1 searches it.
@@ -138,7 +138,7 @@
to suppress solutions arising from earlier searches, as the accumulated cost
(k) can be wrong.*)
fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
- let val countr = ref 0
+ let val countr = Unsynchronized.ref 0
and tf = tracify trace_DEPTH_FIRST (tac1 1)
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
@@ -156,7 +156,7 @@
| depth (bnd,inc) ((k,np,rgd,q)::qs) =
if k>=bnd then depth (bnd,inc) qs
else
- case (countr := !countr+1;
+ case (Unsynchronized.inc countr;
if !trace_DEPTH_FIRST then
tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
else ();
@@ -199,7 +199,7 @@
(*** Best-first search ***)
-val trace_BEST_FIRST = ref false;
+val trace_BEST_FIRST = Unsynchronized.ref false;
(*For creating output sequence*)
fun some_of_list [] = NONE
@@ -273,7 +273,7 @@
fun some_of_list [] = NONE
| some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
-val trace_ASTAR = ref false;
+val trace_ASTAR = Unsynchronized.ref false;
fun THEN_ASTAR tac0 (satp, costf) tac1 =
let val tf = tracify trace_ASTAR tac1;
--- a/src/Pure/simplifier.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/simplifier.ML Tue Sep 29 11:49:22 2009 +0200
@@ -32,7 +32,7 @@
include BASIC_SIMPLIFIER
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
- val debug_bounds: bool ref
+ val debug_bounds: bool Unsynchronized.ref
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
@@ -424,5 +424,5 @@
end;
-structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
-open BasicSimplifier;
+structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
+open Basic_Simplifier;
--- a/src/Pure/tactical.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/tactical.ML Tue Sep 29 11:49:22 2009 +0200
@@ -34,9 +34,9 @@
val RANGE: (int -> tactic) list -> int -> tactic
val print_tac: string -> tactic
val pause_tac: tactic
- val trace_REPEAT: bool ref
- val suppress_tracing: bool ref
- val tracify: bool ref -> tactic -> tactic
+ val trace_REPEAT: bool Unsynchronized.ref
+ val suppress_tracing: bool Unsynchronized.ref
+ val tracify: bool Unsynchronized.ref -> tactic -> tactic
val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
val REPEAT_DETERM_N: int -> tactic -> tactic
@@ -204,16 +204,16 @@
and TRACE_QUIT;
(*Tracing flags*)
-val trace_REPEAT= ref false
-and suppress_tracing = ref false;
+val trace_REPEAT= Unsynchronized.ref false
+and suppress_tracing = Unsynchronized.ref false;
(*Handle all tracing commands for current state and tactic *)
fun exec_trace_command flag (tac, st) =
case TextIO.inputLine TextIO.stdIn of
SOME "\n" => tac st
| SOME "f\n" => Seq.empty
- | SOME "o\n" => (flag:=false; tac st)
- | SOME "s\n" => (suppress_tracing:=true; tac st)
+ | SOME "o\n" => (flag := false; tac st)
+ | SOME "s\n" => (suppress_tracing := true; tac st)
| SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
| SOME "quit\n" => raise TRACE_QUIT
| _ => (tracing
--- a/src/Pure/term.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/term.ML Tue Sep 29 11:49:22 2009 +0200
@@ -112,7 +112,7 @@
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
- val show_question_marks: bool ref
+ val show_question_marks: bool Unsynchronized.ref
end;
signature TERM =
@@ -963,7 +963,7 @@
(* display variables *)
-val show_question_marks = ref true;
+val show_question_marks = Unsynchronized.ref true;
fun string_of_vname (x, i) =
let
--- a/src/Pure/term_subst.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/term_subst.ML Tue Sep 29 11:49:22 2009 +0200
@@ -157,28 +157,32 @@
in
fun instantiateT_maxidx instT ty i =
- let val maxidx = ref i
+ let val maxidx = Unsynchronized.ref i
in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
fun instantiate_maxidx insts tm i =
- let val maxidx = ref i
+ let val maxidx = Unsynchronized.ref i
in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
fun instantiateT [] ty = ty
| instantiateT instT ty =
- (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
+ (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
+ handle Same.SAME => ty);
fun instantiate ([], []) tm = tm
| instantiate insts tm =
- (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
+ (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
+ handle Same.SAME => tm);
fun instantiateT_option [] _ = NONE
| instantiateT_option instT ty =
- (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
+ (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
+ handle Same.SAME => NONE);
fun instantiate_option ([], []) _ = NONE
| instantiate_option insts tm =
- (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
+ (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
+ handle Same.SAME => NONE);
end;
--- a/src/Pure/type.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/type.ML Tue Sep 29 11:49:22 2009 +0200
@@ -417,8 +417,8 @@
(*order-sorted unification*)
fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
let
- val tyvar_count = ref maxidx;
- fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
+ val tyvar_count = Unsynchronized.ref maxidx;
+ fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
fun mg_domain a S = Sorts.mg_domain classes a S
handle Sorts.CLASS_ERROR _ => raise TUNIFY;
--- a/src/Pure/unify.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/unify.ML Tue Sep 29 11:49:22 2009 +0200
@@ -106,7 +106,7 @@
the occurs check must ignore the types of variables. This avoids
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
substitution when ?'a is instantiated with T later. *)
-fun occurs_terms (seen: (indexname list) ref,
+fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
env: Envir.env, v: indexname, ts: term list): bool =
let fun occurs [] = false
| occurs (t::ts) = occur t orelse occurs ts
@@ -160,7 +160,7 @@
Warning: finds a rigid occurrence of ?f in ?f(t).
Should NOT be called in this case: there is a flex-flex unifier
*)
-fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
+fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
else NoOcc
fun occurs [] = NoOcc
@@ -230,7 +230,7 @@
If v occurs nonrigidly then must use full algorithm. *)
fun assignment thy (env, rbinder, t, u) =
let val vT as (v,T) = get_eta_var (rbinder, 0, t)
- in case rigid_occurs_term (ref [], env, v, u) of
+ in case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
NoOcc => let val env = unify_types thy (body_type env T,
fastype env (rbinder,u),env)
in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
@@ -429,7 +429,7 @@
Attempts to update t with u, raising ASSIGN if impossible*)
fun ff_assign thy (env, rbinder, t, u) : Envir.env =
let val vT as (v,T) = get_eta_var(rbinder,0,t)
-in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
+in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
else let val env = unify_types thy (body_type env T,
fastype env (rbinder,u),
env)