1.1 --- a/src/Pure/Concurrent/future.ML Tue Sep 29 11:48:32 2009 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Tue Sep 29 11:49:22 2009 +0200
1.3 @@ -99,13 +99,13 @@
1.4
1.5 (* global state *)
1.6
1.7 -val queue = ref Task_Queue.empty;
1.8 -val next = ref 0;
1.9 -val workers = ref ([]: (Thread.thread * bool) list);
1.10 -val scheduler = ref (NONE: Thread.thread option);
1.11 -val excessive = ref 0;
1.12 -val canceled = ref ([]: Task_Queue.group list);
1.13 -val do_shutdown = ref false;
1.14 +val queue = Unsynchronized.ref Task_Queue.empty;
1.15 +val next = Unsynchronized.ref 0;
1.16 +val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list);
1.17 +val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
1.18 +val excessive = Unsynchronized.ref 0;
1.19 +val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
1.20 +val do_shutdown = Unsynchronized.ref false;
1.21
1.22
1.23 (* synchronization *)
1.24 @@ -162,7 +162,8 @@
1.25 in (result, job) end;
1.26
1.27 fun do_cancel group = (*requires SYNCHRONIZED*)
1.28 - (change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event);
1.29 + (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
1.30 + broadcast scheduler_event);
1.31
1.32 fun execute name (task, group, jobs) =
1.33 let
1.34 @@ -171,7 +172,7 @@
1.35 fold (fn job => fn ok => job valid andalso ok) jobs true) ();
1.36 val _ = SYNCHRONIZED "finish" (fn () =>
1.37 let
1.38 - val maximal = change_result queue (Task_Queue.finish task);
1.39 + val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
1.40 val _ =
1.41 if ok then ()
1.42 else if Task_Queue.cancel (! queue) group then ()
1.43 @@ -188,7 +189,8 @@
1.44 fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
1.45
1.46 fun change_active active = (*requires SYNCHRONIZED*)
1.47 - change workers (AList.update Thread.equal (Thread.self (), active));
1.48 + Unsynchronized.change workers
1.49 + (AList.update Thread.equal (Thread.self (), active));
1.50
1.51
1.52 (* worker threads *)
1.53 @@ -198,14 +200,15 @@
1.54
1.55 fun worker_next () = (*requires SYNCHRONIZED*)
1.56 if ! excessive > 0 then
1.57 - (dec excessive;
1.58 - change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
1.59 + (Unsynchronized.dec excessive;
1.60 + Unsynchronized.change workers
1.61 + (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
1.62 broadcast scheduler_event;
1.63 NONE)
1.64 else if count_active () > Multithreading.max_threads_value () then
1.65 (worker_wait scheduler_event; worker_next ())
1.66 else
1.67 - (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
1.68 + (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
1.69 NONE => (worker_wait work_available; worker_next ())
1.70 | some => some);
1.71
1.72 @@ -215,13 +218,13 @@
1.73 | SOME work => (execute name work; worker_loop name));
1.74
1.75 fun worker_start name = (*requires SYNCHRONIZED*)
1.76 - change workers (cons (SimpleThread.fork false (fn () =>
1.77 + Unsynchronized.change workers (cons (SimpleThread.fork false (fn () =>
1.78 (broadcast scheduler_event; worker_loop name)), true));
1.79
1.80
1.81 (* scheduler *)
1.82
1.83 -val last_status = ref Time.zeroTime;
1.84 +val last_status = Unsynchronized.ref Time.zeroTime;
1.85 val next_status = Time.fromMilliseconds 500;
1.86 val next_round = Time.fromMilliseconds 50;
1.87
1.88 @@ -263,7 +266,8 @@
1.89 val _ = excessive := l - mm;
1.90 val _ =
1.91 if mm > l then
1.92 - funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
1.93 + funpow (mm - l) (fn () =>
1.94 + worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) ()
1.95 else ();
1.96
1.97 (*canceled groups*)
1.98 @@ -272,7 +276,7 @@
1.99 else
1.100 (Multithreading.tracing 1 (fn () =>
1.101 string_of_int (length (! canceled)) ^ " canceled groups");
1.102 - change canceled (filter_out (Task_Queue.cancel (! queue)));
1.103 + Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue)));
1.104 broadcast_work ());
1.105
1.106 (*delay loop*)
1.107 @@ -317,7 +321,8 @@
1.108 val (result, job) = future_job group e;
1.109 val task = SYNCHRONIZED "enqueue" (fn () =>
1.110 let
1.111 - val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
1.112 + val (task, minimal) =
1.113 + Unsynchronized.change_result queue (Task_Queue.enqueue group deps pri job);
1.114 val _ = if minimal then signal work_available else ();
1.115 val _ = scheduler_check ();
1.116 in task end);
1.117 @@ -347,7 +352,7 @@
1.118 fun join_next deps = (*requires SYNCHRONIZED*)
1.119 if null deps then NONE
1.120 else
1.121 - (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
1.122 + (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
1.123 (NONE, []) => NONE
1.124 | (NONE, deps') => (worker_wait work_finished; join_next deps')
1.125 | (SOME work, deps') => SOME (work, deps'));
2.1 --- a/src/Pure/Concurrent/synchronized.ML Tue Sep 29 11:48:32 2009 +0200
2.2 +++ b/src/Pure/Concurrent/synchronized.ML Tue Sep 29 11:49:22 2009 +0200
2.3 @@ -24,13 +24,13 @@
2.4 {name: string,
2.5 lock: Mutex.mutex,
2.6 cond: ConditionVar.conditionVar,
2.7 - var: 'a ref};
2.8 + var: 'a Unsynchronized.ref};
2.9
2.10 fun var name x = Var
2.11 {name = name,
2.12 lock = Mutex.mutex (),
2.13 cond = ConditionVar.conditionVar (),
2.14 - var = ref x};
2.15 + var = Unsynchronized.ref x};
2.16
2.17 fun value (Var {var, ...}) = ! var;
2.18
3.1 --- a/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 11:48:32 2009 +0200
3.2 +++ b/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 11:49:22 2009 +0200
3.3 @@ -7,9 +7,9 @@
3.4 structure Synchronized: SYNCHRONIZED =
3.5 struct
3.6
3.7 -datatype 'a var = Var of 'a ref;
3.8 +datatype 'a var = Var of 'a Unsynchronized.ref;
3.9
3.10 -fun var _ x = Var (ref x);
3.11 +fun var _ x = Var (Unsynchronized.ref x);
3.12 fun value (Var var) = ! var;
3.13
3.14 fun timed_access (Var var) _ f =
4.1 --- a/src/Pure/General/file.ML Tue Sep 29 11:48:32 2009 +0200
4.2 +++ b/src/Pure/General/file.ML Tue Sep 29 11:49:22 2009 +0200
4.3 @@ -85,7 +85,8 @@
4.4 (* file identification *)
4.5
4.6 local
4.7 - val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
4.8 + val ident_cache =
4.9 + Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
4.10 in
4.11
4.12 fun check_cache (path, time) = CRITICAL (fn () =>
4.13 @@ -94,7 +95,8 @@
4.14 | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
4.15
4.16 fun update_cache (path, (time, id)) = CRITICAL (fn () =>
4.17 - change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
4.18 + Unsynchronized.change ident_cache
4.19 + (Symtab.update (path, {time_stamp = time, id = id})));
4.20
4.21 end;
4.22
5.1 --- a/src/Pure/General/lazy.ML Tue Sep 29 11:48:32 2009 +0200
5.2 +++ b/src/Pure/General/lazy.ML Tue Sep 29 11:49:22 2009 +0200
5.3 @@ -26,12 +26,12 @@
5.4 Lazy of unit -> 'a |
5.5 Result of 'a Exn.result;
5.6
5.7 -type 'a lazy = 'a T ref;
5.8 +type 'a lazy = 'a T Unsynchronized.ref;
5.9
5.10 fun same (r1: 'a lazy, r2) = r1 = r2;
5.11
5.12 -fun lazy e = ref (Lazy e);
5.13 -fun value x = ref (Result (Exn.Result x));
5.14 +fun lazy e = Unsynchronized.ref (Lazy e);
5.15 +fun value x = Unsynchronized.ref (Result (Exn.Result x));
5.16
5.17 fun peek r =
5.18 (case ! r of
6.1 --- a/src/Pure/General/markup.ML Tue Sep 29 11:48:32 2009 +0200
6.2 +++ b/src/Pure/General/markup.ML Tue Sep 29 11:49:22 2009 +0200
6.3 @@ -323,10 +323,10 @@
6.4
6.5 local
6.6 val default = {output = default_output};
6.7 - val modes = ref (Symtab.make [("", default)]);
6.8 + val modes = Unsynchronized.ref (Symtab.make [("", default)]);
6.9 in
6.10 fun add_mode name output = CRITICAL (fn () =>
6.11 - change modes (Symtab.update_new (name, {output = output})));
6.12 + Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
6.13 fun get_mode () =
6.14 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
6.15 end;
7.1 --- a/src/Pure/General/name_space.ML Tue Sep 29 11:48:32 2009 +0200
7.2 +++ b/src/Pure/General/name_space.ML Tue Sep 29 11:49:22 2009 +0200
7.3 @@ -9,9 +9,9 @@
7.4
7.5 signature BASIC_NAME_SPACE =
7.6 sig
7.7 - val long_names: bool ref
7.8 - val short_names: bool ref
7.9 - val unique_names: bool ref
7.10 + val long_names: bool Unsynchronized.ref
7.11 + val short_names: bool Unsynchronized.ref
7.12 + val unique_names: bool Unsynchronized.ref
7.13 end;
7.14
7.15 signature NAME_SPACE =
7.16 @@ -105,9 +105,9 @@
7.17 else ext (get_accesses space name)
7.18 end;
7.19
7.20 -val long_names = ref false;
7.21 -val short_names = ref false;
7.22 -val unique_names = ref true;
7.23 +val long_names = Unsynchronized.ref false;
7.24 +val short_names = Unsynchronized.ref false;
7.25 +val unique_names = Unsynchronized.ref true;
7.26
7.27 fun extern space name =
7.28 extern_flags
7.29 @@ -261,6 +261,6 @@
7.30
7.31 end;
7.32
7.33 -structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
7.34 -open BasicNameSpace;
7.35 +structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
7.36 +open Basic_Name_Space;
7.37
8.1 --- a/src/Pure/General/output.ML Tue Sep 29 11:48:32 2009 +0200
8.2 +++ b/src/Pure/General/output.ML Tue Sep 29 11:49:22 2009 +0200
8.3 @@ -11,13 +11,13 @@
8.4 val priority: string -> unit
8.5 val tracing: string -> unit
8.6 val warning: string -> unit
8.7 - val tolerate_legacy_features: bool ref
8.8 + val tolerate_legacy_features: bool Unsynchronized.ref
8.9 val legacy_feature: string -> unit
8.10 val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
8.11 val timeit: (unit -> 'a) -> 'a
8.12 val timeap: ('a -> 'b) -> 'a -> 'b
8.13 val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
8.14 - val timing: bool ref
8.15 + val timing: bool Unsynchronized.ref
8.16 end;
8.17
8.18 signature OUTPUT =
8.19 @@ -32,18 +32,18 @@
8.20 val std_output: output -> unit
8.21 val std_error: output -> unit
8.22 val writeln_default: output -> unit
8.23 - val writeln_fn: (output -> unit) ref
8.24 - val priority_fn: (output -> unit) ref
8.25 - val tracing_fn: (output -> unit) ref
8.26 - val warning_fn: (output -> unit) ref
8.27 - val error_fn: (output -> unit) ref
8.28 - val debug_fn: (output -> unit) ref
8.29 - val prompt_fn: (output -> unit) ref
8.30 - val status_fn: (output -> unit) ref
8.31 + val writeln_fn: (output -> unit) Unsynchronized.ref
8.32 + val priority_fn: (output -> unit) Unsynchronized.ref
8.33 + val tracing_fn: (output -> unit) Unsynchronized.ref
8.34 + val warning_fn: (output -> unit) Unsynchronized.ref
8.35 + val error_fn: (output -> unit) Unsynchronized.ref
8.36 + val debug_fn: (output -> unit) Unsynchronized.ref
8.37 + val prompt_fn: (output -> unit) Unsynchronized.ref
8.38 + val status_fn: (output -> unit) Unsynchronized.ref
8.39 val error_msg: string -> unit
8.40 val prompt: string -> unit
8.41 val status: string -> unit
8.42 - val debugging: bool ref
8.43 + val debugging: bool Unsynchronized.ref
8.44 val no_warnings: ('a -> 'b) -> 'a -> 'b
8.45 val debug: (unit -> string) -> unit
8.46 end;
8.47 @@ -60,10 +60,10 @@
8.48
8.49 local
8.50 val default = {output = default_output, escape = default_escape};
8.51 - val modes = ref (Symtab.make [("", default)]);
8.52 + val modes = Unsynchronized.ref (Symtab.make [("", default)]);
8.53 in
8.54 fun add_mode name output escape = CRITICAL (fn () =>
8.55 - change modes (Symtab.update_new (name, {output = output, escape = escape})));
8.56 + Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
8.57 fun get_mode () =
8.58 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
8.59 end;
8.60 @@ -91,14 +91,14 @@
8.61
8.62 (* Isabelle output channels *)
8.63
8.64 -val writeln_fn = ref writeln_default;
8.65 -val priority_fn = ref (fn s => ! writeln_fn s);
8.66 -val tracing_fn = ref (fn s => ! writeln_fn s);
8.67 -val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
8.68 -val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
8.69 -val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
8.70 -val prompt_fn = ref std_output;
8.71 -val status_fn = ref (fn _: string => ());
8.72 +val writeln_fn = Unsynchronized.ref writeln_default;
8.73 +val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
8.74 +val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
8.75 +val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
8.76 +val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
8.77 +val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
8.78 +val prompt_fn = Unsynchronized.ref std_output;
8.79 +val status_fn = Unsynchronized.ref (fn _: string => ());
8.80
8.81 fun writeln s = ! writeln_fn (output s);
8.82 fun priority s = ! priority_fn (output s);
8.83 @@ -108,13 +108,13 @@
8.84 fun prompt s = ! prompt_fn (output s);
8.85 fun status s = ! status_fn (output s);
8.86
8.87 -val tolerate_legacy_features = ref true;
8.88 +val tolerate_legacy_features = Unsynchronized.ref true;
8.89 fun legacy_feature s =
8.90 (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
8.91
8.92 fun no_warnings f = setmp warning_fn (K ()) f;
8.93
8.94 -val debugging = ref false;
8.95 +val debugging = Unsynchronized.ref false;
8.96 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
8.97
8.98
8.99 @@ -140,9 +140,9 @@
8.100 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
8.101
8.102 (*global timing mode*)
8.103 -val timing = ref false;
8.104 +val timing = Unsynchronized.ref false;
8.105
8.106 end;
8.107
8.108 -structure BasicOutput: BASIC_OUTPUT = Output;
8.109 -open BasicOutput;
8.110 +structure Basic_Output: BASIC_OUTPUT = Output;
8.111 +open Basic_Output;
9.1 --- a/src/Pure/General/pretty.ML Tue Sep 29 11:48:32 2009 +0200
9.2 +++ b/src/Pure/General/pretty.ML Tue Sep 29 11:49:22 2009 +0200
9.3 @@ -86,10 +86,10 @@
9.4
9.5 local
9.6 val default = {indent = default_indent};
9.7 - val modes = ref (Symtab.make [("", default)]);
9.8 + val modes = Unsynchronized.ref (Symtab.make [("", default)]);
9.9 in
9.10 fun add_mode name indent = CRITICAL (fn () =>
9.11 - change modes (Symtab.update_new (name, {indent = indent})));
9.12 + Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
9.13 fun get_mode () =
9.14 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
9.15 end;
9.16 @@ -186,14 +186,14 @@
9.17 breakgain = m div 20, (*minimum added space required of a break*)
9.18 emergencypos = m div 2}; (*position too far to right*)
9.19
9.20 -val margin_info = ref (make_margin_info 76);
9.21 +val margin_info = Unsynchronized.ref (make_margin_info 76);
9.22 fun setmargin m = margin_info := make_margin_info m;
9.23 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
9.24
9.25
9.26 (* depth limitation *)
9.27
9.28 -val depth = ref 0; (*maximum depth; 0 means no limit*)
9.29 +val depth = Unsynchronized.ref 0; (*maximum depth; 0 means no limit*)
9.30 fun setdepth dp = (depth := dp);
9.31
9.32 local
10.1 --- a/src/Pure/General/print_mode.ML Tue Sep 29 11:48:32 2009 +0200
10.2 +++ b/src/Pure/General/print_mode.ML Tue Sep 29 11:49:22 2009 +0200
10.3 @@ -7,9 +7,9 @@
10.4
10.5 signature BASIC_PRINT_MODE =
10.6 sig
10.7 - val print_mode: string list ref (*global template*)
10.8 - val print_mode_value: unit -> string list (*thread-local value*)
10.9 - val print_mode_active: string -> bool (*thread-local value*)
10.10 + val print_mode: string list Unsynchronized.ref (*global template*)
10.11 + val print_mode_value: unit -> string list (*thread-local value*)
10.12 + val print_mode_active: string -> bool (*thread-local value*)
10.13 end;
10.14
10.15 signature PRINT_MODE =
10.16 @@ -28,7 +28,7 @@
10.17 val input = "input";
10.18 val internal = "internal";
10.19
10.20 -val print_mode = ref ([]: string list);
10.21 +val print_mode = Unsynchronized.ref ([]: string list);
10.22 val tag = Universal.tag () : string list option Universal.tag;
10.23
10.24 fun print_mode_value () =
11.1 --- a/src/Pure/General/secure.ML Tue Sep 29 11:48:32 2009 +0200
11.2 +++ b/src/Pure/General/secure.ML Tue Sep 29 11:49:22 2009 +0200
11.3 @@ -23,7 +23,7 @@
11.4
11.5 (** secure flag **)
11.6
11.7 -val secure = ref false;
11.8 +val secure = Unsynchronized.ref false;
11.9
11.10 fun set_secure () = secure := true;
11.11 fun is_secure () = ! secure;
12.1 --- a/src/Pure/Isar/code.ML Tue Sep 29 11:48:32 2009 +0200
12.2 +++ b/src/Pure/Isar/code.ML Tue Sep 29 11:49:22 2009 +0200
12.3 @@ -217,8 +217,8 @@
12.4 purge: theory -> string list -> Object.T -> Object.T
12.5 };
12.6
12.7 -val kinds = ref (Datatab.empty: kind Datatab.table);
12.8 -val kind_keys = ref ([]: serial list);
12.9 +val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
12.10 +val kind_keys = Unsynchronized.ref ([]: serial list);
12.11
12.12 fun invoke f k = case Datatab.lookup (! kinds) k
12.13 of SOME kind => f kind
12.14 @@ -230,8 +230,8 @@
12.15 let
12.16 val k = serial ();
12.17 val kind = {empty = empty, purge = purge};
12.18 - val _ = change kinds (Datatab.update (k, kind));
12.19 - val _ = change kind_keys (cons k);
12.20 + val _ = Unsynchronized.change kinds (Datatab.update (k, kind));
12.21 + val _ = Unsynchronized.change kind_keys (cons k);
12.22 in k end;
12.23
12.24 fun invoke_init k = invoke (fn kind => #empty kind) k;
12.25 @@ -252,13 +252,13 @@
12.26
12.27 structure Code_Data = TheoryDataFun
12.28 (
12.29 - type T = spec * data ref;
12.30 + type T = spec * data Unsynchronized.ref;
12.31 val empty = (make_spec (false,
12.32 - (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
12.33 - fun copy (spec, data) = (spec, ref (! data));
12.34 + (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
12.35 + fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
12.36 val extend = copy;
12.37 fun merge pp ((spec1, data1), (spec2, data2)) =
12.38 - (merge_spec (spec1, spec2), ref empty_data);
12.39 + (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
12.40 );
12.41
12.42 fun thy_data f thy = f ((snd o Code_Data.get) thy);
12.43 @@ -267,7 +267,7 @@
12.44 case Datatab.lookup (! data_ref) kind
12.45 of SOME x => x
12.46 | NONE => let val y = invoke_init kind
12.47 - in (change data_ref (Datatab.update (kind, y)); y) end;
12.48 + in (Unsynchronized.change data_ref (Datatab.update (kind, y)); y) end;
12.49
12.50 in
12.51
12.52 @@ -281,11 +281,11 @@
12.53 | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
12.54
12.55 fun map_exec_purge touched f thy =
12.56 - Code_Data.map (fn (exec, data) => (f exec, ref (case touched
12.57 + Code_Data.map (fn (exec, data) => (f exec, Unsynchronized.ref (case touched
12.58 of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
12.59 | NONE => empty_data))) thy;
12.60
12.61 -val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
12.62 +val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data));
12.63
12.64 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
12.65 o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
12.66 @@ -332,7 +332,7 @@
12.67 let
12.68 val data = get_ensure_init kind data_ref;
12.69 val data' = f (dest data);
12.70 - in (change data_ref (Datatab.update (kind, mk data')); data') end;
12.71 + in (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
12.72 in thy_data chnge end;
12.73
12.74 fun change_yield_data (kind, mk, dest) =
12.75 @@ -341,7 +341,7 @@
12.76 let
12.77 val data = get_ensure_init kind data_ref;
12.78 val (x, data') = f (dest data);
12.79 - in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
12.80 + in (x, (Unsynchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
12.81 in thy_data chnge end;
12.82
12.83 end; (*local*)
13.1 --- a/src/Pure/Isar/isar_document.ML Tue Sep 29 11:48:32 2009 +0200
13.2 +++ b/src/Pure/Isar/isar_document.ML Tue Sep 29 11:49:22 2009 +0200
13.3 @@ -112,18 +112,18 @@
13.4 (** global configuration **)
13.5
13.6 local
13.7 - val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
13.8 - val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
13.9 - val global_documents = ref (Symtab.empty: document Symtab.table);
13.10 + val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
13.11 + val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
13.12 + val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
13.13 in
13.14
13.15 -fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
13.16 +fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
13.17 fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
13.18
13.19 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
13.20 +fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
13.21 fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
13.22
13.23 -fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
13.24 +fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
13.25 fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
13.26
13.27 fun init () = NAMED_CRITICAL "Isar" (fn () =>
14.1 --- a/src/Pure/Isar/local_syntax.ML Tue Sep 29 11:48:32 2009 +0200
14.2 +++ b/src/Pure/Isar/local_syntax.ML Tue Sep 29 11:49:22 2009 +0200
14.3 @@ -4,7 +4,7 @@
14.4 Local syntax depending on theory syntax.
14.5 *)
14.6
14.7 -val show_structs = ref false;
14.8 +val show_structs = Unsynchronized.ref false;
14.9
14.10 signature LOCAL_SYNTAX =
14.11 sig
15.1 --- a/src/Pure/Isar/method.ML Tue Sep 29 11:48:32 2009 +0200
15.2 +++ b/src/Pure/Isar/method.ML Tue Sep 29 11:49:22 2009 +0200
15.3 @@ -8,7 +8,7 @@
15.4 sig
15.5 val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
15.6 val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
15.7 - val trace_rules: bool ref
15.8 + val trace_rules: bool Unsynchronized.ref
15.9 end;
15.10
15.11 signature METHOD =
15.12 @@ -215,7 +215,7 @@
15.13
15.14 (* rule etc. -- single-step refinements *)
15.15
15.16 -val trace_rules = ref false;
15.17 +val trace_rules = Unsynchronized.ref false;
15.18
15.19 fun trace ctxt rules =
15.20 if ! trace_rules andalso not (null rules) then
16.1 --- a/src/Pure/Isar/outer_keyword.ML Tue Sep 29 11:48:32 2009 +0200
16.2 +++ b/src/Pure/Isar/outer_keyword.ML Tue Sep 29 11:49:22 2009 +0200
16.3 @@ -116,16 +116,16 @@
16.4
16.5 local
16.6
16.7 -val global_commands = ref (Symtab.empty: T Symtab.table);
16.8 -val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
16.9 +val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
16.10 +val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
16.11
16.12 in
16.13
16.14 fun get_commands () = CRITICAL (fn () => ! global_commands);
16.15 fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
16.16
16.17 -fun change_commands f = CRITICAL (fn () => change global_commands f);
16.18 -fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
16.19 +fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
16.20 +fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
16.21
16.22 end;
16.23
17.1 --- a/src/Pure/Isar/outer_lex.ML Tue Sep 29 11:48:32 2009 +0200
17.2 +++ b/src/Pure/Isar/outer_lex.ML Tue Sep 29 11:49:22 2009 +0200
17.3 @@ -83,7 +83,7 @@
17.4 datatype slot =
17.5 Slot |
17.6 Value of value option |
17.7 - Assignable of value option ref;
17.8 + Assignable of value option Unsynchronized.ref;
17.9
17.10
17.11 (* datatype token *)
17.12 @@ -245,7 +245,7 @@
17.13 (* static binding *)
17.14
17.15 (*1st stage: make empty slots assignable*)
17.16 -fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
17.17 +fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
17.18 | assignable tok = tok;
17.19
17.20 (*2nd stage: assign values as side-effect of scanning*)
17.21 @@ -253,7 +253,7 @@
17.22 | assign _ _ = ();
17.23
17.24 (*3rd stage: static closure of final values*)
17.25 -fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
17.26 +fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
17.27 | closure tok = tok;
17.28
17.29
18.1 --- a/src/Pure/Isar/outer_syntax.ML Tue Sep 29 11:48:32 2009 +0200
18.2 +++ b/src/Pure/Isar/outer_syntax.ML Tue Sep 29 11:49:22 2009 +0200
18.3 @@ -88,11 +88,11 @@
18.4
18.5 local
18.6
18.7 -val global_commands = ref (Symtab.empty: command Symtab.table);
18.8 -val global_markups = ref ([]: (string * ThyOutput.markup) list);
18.9 +val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
18.10 +val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
18.11
18.12 fun change_commands f = CRITICAL (fn () =>
18.13 - (change global_commands f;
18.14 + (Unsynchronized.change global_commands f;
18.15 global_markups :=
18.16 Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
18.17 (! global_commands) []));
19.1 --- a/src/Pure/Isar/proof.ML Tue Sep 29 11:48:32 2009 +0200
19.2 +++ b/src/Pure/Isar/proof.ML Tue Sep 29 11:49:22 2009 +0200
19.3 @@ -30,8 +30,8 @@
19.4 val enter_forward: state -> state
19.5 val goal_message: (unit -> Pretty.T) -> state -> state
19.6 val get_goal: state -> context * (thm list * thm)
19.7 - val show_main_goal: bool ref
19.8 - val verbose: bool ref
19.9 + val show_main_goal: bool Unsynchronized.ref
19.10 + val verbose: bool Unsynchronized.ref
19.11 val pretty_state: int -> state -> Pretty.T list
19.12 val pretty_goals: bool -> state -> Pretty.T list
19.13 val refine: Method.text -> state -> state Seq.seq
19.14 @@ -315,7 +315,7 @@
19.15
19.16 (** pretty_state **)
19.17
19.18 -val show_main_goal = ref false;
19.19 +val show_main_goal = Unsynchronized.ref false;
19.20 val verbose = ProofContext.verbose;
19.21
19.22 fun pretty_facts _ _ NONE = []
19.23 @@ -930,8 +930,8 @@
19.24
19.25 fun gen_show prep_att prepp before_qed after_qed stmt int state =
19.26 let
19.27 - val testing = ref false;
19.28 - val rule = ref (NONE: thm option);
19.29 + val testing = Unsynchronized.ref false;
19.30 + val rule = Unsynchronized.ref (NONE: thm option);
19.31 fun fail_msg ctxt =
19.32 "Local statement will fail to refine any pending goal" ::
19.33 (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
20.1 --- a/src/Pure/Isar/proof_context.ML Tue Sep 29 11:48:32 2009 +0200
20.2 +++ b/src/Pure/Isar/proof_context.ML Tue Sep 29 11:49:22 2009 +0200
20.3 @@ -123,15 +123,15 @@
20.4 val add_abbrev: string -> Properties.T ->
20.5 binding * term -> Proof.context -> (term * term) * Proof.context
20.6 val revert_abbrev: string -> string -> Proof.context -> Proof.context
20.7 - val verbose: bool ref
20.8 + val verbose: bool Unsynchronized.ref
20.9 val setmp_verbose: ('a -> 'b) -> 'a -> 'b
20.10 val print_syntax: Proof.context -> unit
20.11 val print_abbrevs: Proof.context -> unit
20.12 val print_binds: Proof.context -> unit
20.13 val print_lthms: Proof.context -> unit
20.14 val print_cases: Proof.context -> unit
20.15 - val debug: bool ref
20.16 - val prems_limit: int ref
20.17 + val debug: bool Unsynchronized.ref
20.18 + val prems_limit: int Unsynchronized.ref
20.19 val pretty_ctxt: Proof.context -> Pretty.T list
20.20 val pretty_context: Proof.context -> Pretty.T list
20.21 val query_type: Proof.context -> string -> Properties.T
20.22 @@ -1208,9 +1208,9 @@
20.23
20.24 (** print context information **)
20.25
20.26 -val debug = ref false;
20.27 +val debug = Unsynchronized.ref false;
20.28
20.29 -val verbose = ref false;
20.30 +val verbose = Unsynchronized.ref false;
20.31 fun verb f x = if ! verbose then f (x ()) else [];
20.32
20.33 fun setmp_verbose f x = Library.setmp verbose true f x;
20.34 @@ -1320,7 +1320,7 @@
20.35
20.36 (* core context *)
20.37
20.38 -val prems_limit = ref ~1;
20.39 +val prems_limit = Unsynchronized.ref ~1;
20.40
20.41 fun pretty_ctxt ctxt =
20.42 if ! prems_limit < 0 andalso not (! debug) then []
21.1 --- a/src/Pure/Isar/toplevel.ML Tue Sep 29 11:48:32 2009 +0200
21.2 +++ b/src/Pure/Isar/toplevel.ML Tue Sep 29 11:49:22 2009 +0200
21.3 @@ -24,12 +24,12 @@
21.4 val enter_proof_body: state -> Proof.state
21.5 val print_state_context: state -> unit
21.6 val print_state: bool -> state -> unit
21.7 - val quiet: bool ref
21.8 - val debug: bool ref
21.9 - val interact: bool ref
21.10 - val timing: bool ref
21.11 - val profiling: int ref
21.12 - val skip_proofs: bool ref
21.13 + val quiet: bool Unsynchronized.ref
21.14 + val debug: bool Unsynchronized.ref
21.15 + val interact: bool Unsynchronized.ref
21.16 + val timing: bool Unsynchronized.ref
21.17 + val profiling: int Unsynchronized.ref
21.18 + val skip_proofs: bool Unsynchronized.ref
21.19 exception TERMINATE
21.20 exception TOPLEVEL_ERROR
21.21 val program: (unit -> 'a) -> 'a
21.22 @@ -216,12 +216,12 @@
21.23
21.24 (** toplevel transitions **)
21.25
21.26 -val quiet = ref false;
21.27 +val quiet = Unsynchronized.ref false;
21.28 val debug = Output.debugging;
21.29 -val interact = ref false;
21.30 +val interact = Unsynchronized.ref false;
21.31 val timing = Output.timing;
21.32 -val profiling = ref 0;
21.33 -val skip_proofs = ref false;
21.34 +val profiling = Unsynchronized.ref 0;
21.35 +val skip_proofs = Unsynchronized.ref false;
21.36
21.37 exception TERMINATE = Runtime.TERMINATE;
21.38 exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
21.39 @@ -550,9 +550,9 @@
21.40
21.41 (* post-transition hooks *)
21.42
21.43 -local val hooks = ref ([]: (transition -> state -> state -> unit) list) in
21.44 +local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
21.45
21.46 -fun add_hook f = CRITICAL (fn () => change hooks (cons f));
21.47 +fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
21.48 fun get_hooks () = CRITICAL (fn () => ! hooks);
21.49
21.50 end;
22.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 11:48:32 2009 +0200
22.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Sep 29 11:49:22 2009 +0200
22.3 @@ -5,11 +5,11 @@
22.4
22.5 fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
22.6 let
22.7 - val in_buffer = ref (explode (tune_source txt));
22.8 - val out_buffer = ref ([]: string list);
22.9 + val in_buffer = Unsynchronized.ref (explode (tune_source txt));
22.10 + val out_buffer = Unsynchronized.ref ([]: string list);
22.11 fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
22.12
22.13 - val current_line = ref line;
22.14 + val current_line = Unsynchronized.ref line;
22.15 fun get () =
22.16 (case ! in_buffer of
22.17 [] => ""
23.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 11:48:32 2009 +0200
23.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Sep 29 11:49:22 2009 +0200
23.3 @@ -14,9 +14,9 @@
23.4 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
23.5 (start_line, name) verbose txt =
23.6 let
23.7 - val current_line = ref start_line;
23.8 - val in_buffer = ref (String.explode (tune_source txt));
23.9 - val out_buffer = ref ([]: string list);
23.10 + val current_line = Unsynchronized.ref start_line;
23.11 + val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
23.12 + val out_buffer = Unsynchronized.ref ([]: string list);
23.13 fun output () = drop_newline (implode (rev (! out_buffer)));
23.14
23.15 fun get () =
24.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 11:48:32 2009 +0200
24.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Sep 29 11:49:22 2009 +0200
24.3 @@ -14,9 +14,9 @@
24.4 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
24.5 (start_line, name) verbose txt =
24.6 let
24.7 - val line = ref start_line;
24.8 - val in_buffer = ref (String.explode (tune_source txt));
24.9 - val out_buffer = ref ([]: string list);
24.10 + val line = Unsynchronized.ref start_line;
24.11 + val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
24.12 + val out_buffer = Unsynchronized.ref ([]: string list);
24.13 fun output () = drop_newline (implode (rev (! out_buffer)));
24.14
24.15 fun get () =
25.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 11:48:32 2009 +0200
25.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Sep 29 11:49:22 2009 +0200
25.3 @@ -31,7 +31,7 @@
25.4
25.5 val available = true;
25.6
25.7 -val max_threads = ref 0;
25.8 +val max_threads = Unsynchronized.ref 0;
25.9
25.10 val tested_platform =
25.11 let val ml_platform = getenv "ML_PLATFORM"
25.12 @@ -114,7 +114,7 @@
25.13
25.14 (* tracing *)
25.15
25.16 -val trace = ref 0;
25.17 +val trace = Unsynchronized.ref 0;
25.18
25.19 fun tracing level msg =
25.20 if level > ! trace then ()
25.21 @@ -148,7 +148,7 @@
25.22 fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
25.23 let
25.24 val worker = Thread.self ();
25.25 - val timeout = ref false;
25.26 + val timeout = Unsynchronized.ref false;
25.27 val watchdog = Thread.fork (fn () =>
25.28 (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
25.29
25.30 @@ -173,7 +173,7 @@
25.31
25.32 (*result state*)
25.33 datatype result = Wait | Signal | Result of int;
25.34 - val result = ref Wait;
25.35 + val result = Unsynchronized.ref Wait;
25.36 val lock = Mutex.mutex ();
25.37 val cond = ConditionVar.conditionVar ();
25.38 fun set_result res =
25.39 @@ -231,8 +231,8 @@
25.40 local
25.41
25.42 val critical_lock = Mutex.mutex ();
25.43 -val critical_thread = ref (NONE: Thread.thread option);
25.44 -val critical_name = ref "";
25.45 +val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
25.46 +val critical_name = Unsynchronized.ref "";
25.47
25.48 in
25.49
25.50 @@ -274,7 +274,7 @@
25.51 local
25.52
25.53 val serial_lock = Mutex.mutex ();
25.54 -val serial_count = ref 0;
25.55 +val serial_count = Unsynchronized.ref 0;
25.56
25.57 in
25.58
26.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 11:48:32 2009 +0200
26.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 29 11:49:22 2009 +0200
26.3 @@ -91,8 +91,8 @@
26.4 if null toks then Position.none
26.5 else ML_Lex.end_pos_of (List.last toks);
26.6
26.7 - val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
26.8 - val line = ref (the_default 1 (Position.line_of pos));
26.9 + val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
26.10 + val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
26.11
26.12 fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
26.13 fun get () =
26.14 @@ -106,9 +106,9 @@
26.15
26.16 (* output *)
26.17
26.18 - val output_buffer = ref Buffer.empty;
26.19 + val output_buffer = Unsynchronized.ref Buffer.empty;
26.20 fun output () = Buffer.content (! output_buffer);
26.21 - fun put s = change output_buffer (Buffer.add s);
26.22 + fun put s = Unsynchronized.change output_buffer (Buffer.add s);
26.23
26.24 fun put_message {message, hard, location, context = _} =
26.25 (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
27.1 --- a/src/Pure/ML/ml_context.ML Tue Sep 29 11:48:32 2009 +0200
27.2 +++ b/src/Pure/ML/ml_context.ML Tue Sep 29 11:49:22 2009 +0200
27.3 @@ -19,20 +19,21 @@
27.4 val the_global_context: unit -> theory
27.5 val the_local_context: unit -> Proof.context
27.6 val exec: (unit -> unit) -> Context.generic -> Context.generic
27.7 - val stored_thms: thm list ref
27.8 + val stored_thms: thm list Unsynchronized.ref
27.9 val ml_store_thm: string * thm -> unit
27.10 val ml_store_thms: string * thm list -> unit
27.11 type antiq =
27.12 {struct_name: string, background: Proof.context} ->
27.13 (Proof.context -> string * string) * Proof.context
27.14 val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
27.15 - val trace: bool ref
27.16 + val trace: bool Unsynchronized.ref
27.17 val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
27.18 Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
27.19 val eval: bool -> Position.T -> Symbol_Pos.text -> unit
27.20 val eval_file: Path.T -> unit
27.21 val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
27.22 - val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
27.23 + val evaluate: Proof.context -> bool ->
27.24 + string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
27.25 val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
27.26 end
27.27
27.28 @@ -53,7 +54,7 @@
27.29
27.30 (* theorem bindings *)
27.31
27.32 -val stored_thms: thm list ref = ref [];
27.33 +val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
27.34
27.35 fun ml_store sel (name, ths) =
27.36 let
27.37 @@ -89,12 +90,13 @@
27.38
27.39 local
27.40
27.41 -val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
27.42 +val global_parsers =
27.43 + Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
27.44
27.45 in
27.46
27.47 fun add_antiq name scan = CRITICAL (fn () =>
27.48 - change global_parsers (fn tab =>
27.49 + Unsynchronized.change global_parsers (fn tab =>
27.50 (if not (Symtab.defined tab name) then ()
27.51 else warning ("Redefined ML antiquotation: " ^ quote name);
27.52 Symtab.update (name, scan) tab)));
27.53 @@ -162,7 +164,7 @@
27.54 in (ml, SOME (Context.Proof ctxt')) end;
27.55 in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
27.56
27.57 -val trace = ref false;
27.58 +val trace = Unsynchronized.ref false;
27.59
27.60 fun eval verbose pos txt =
27.61 let
28.1 --- a/src/Pure/Proof/extraction.ML Tue Sep 29 11:48:32 2009 +0200
28.2 +++ b/src/Pure/Proof/extraction.ML Tue Sep 29 11:49:22 2009 +0200
28.3 @@ -91,7 +91,7 @@
28.4 Pattern.rewrite_term thy [] (condrew' :: procs) tm
28.5 and condrew' tm =
28.6 let
28.7 - val cache = ref ([] : (term * term) list);
28.8 + val cache = Unsynchronized.ref ([] : (term * term) list);
28.9 fun lookup f x = (case AList.lookup (op =) (!cache) x of
28.10 NONE =>
28.11 let val y = f x
29.1 --- a/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:48:32 2009 +0200
29.2 +++ b/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:49:22 2009 +0200
29.3 @@ -6,7 +6,7 @@
29.4
29.5 signature RECONSTRUCT =
29.6 sig
29.7 - val quiet_mode : bool ref
29.8 + val quiet_mode : bool Unsynchronized.ref
29.9 val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
29.10 val prop_of' : term list -> Proofterm.proof -> term
29.11 val prop_of : Proofterm.proof -> term
29.12 @@ -19,7 +19,7 @@
29.13
29.14 open Proofterm;
29.15
29.16 -val quiet_mode = ref true;
29.17 +val quiet_mode = Unsynchronized.ref true;
29.18 fun message s = if !quiet_mode then () else writeln s;
29.19
29.20 fun vars_of t = map Var (rev (Term.add_vars t []));
30.1 --- a/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 11:48:32 2009 +0200
30.2 +++ b/src/Pure/ProofGeneral/preferences.ML Tue Sep 29 11:49:22 2009 +0200
30.3 @@ -18,11 +18,11 @@
30.4 get: unit -> string,
30.5 set: string -> unit}
30.6 val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
30.7 - 'a ref -> string -> string -> preference
30.8 - val string_pref: string ref -> string -> string -> preference
30.9 - val int_pref: int ref -> string -> string -> preference
30.10 - val nat_pref: int ref -> string -> string -> preference
30.11 - val bool_pref: bool ref -> string -> string -> preference
30.12 + 'a Unsynchronized.ref -> string -> string -> preference
30.13 + val string_pref: string Unsynchronized.ref -> string -> string -> preference
30.14 + val int_pref: int Unsynchronized.ref -> string -> string -> preference
30.15 + val nat_pref: int Unsynchronized.ref -> string -> string -> preference
30.16 + val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
30.17 type T = (string * preference list) list
30.18 val pure_preferences: T
30.19 val remove: string -> T -> T
30.20 @@ -95,8 +95,9 @@
30.21 let
30.22 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
30.23 fun set s =
30.24 - if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN)
30.25 - else change print_mode (remove (op =) thm_depsN);
30.26 + if PgipTypes.read_pgipbool s
30.27 + then Unsynchronized.change print_mode (insert (op =) thm_depsN)
30.28 + else Unsynchronized.change print_mode (remove (op =) thm_depsN);
30.29 in
30.30 mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
30.31 "Track theorem dependencies within Proof General"
31.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 11:48:32 2009 +0200
31.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 29 11:49:22 2009 +0200
31.3 @@ -226,7 +226,7 @@
31.4
31.5 (* init *)
31.6
31.7 -val initialized = ref false;
31.8 +val initialized = Unsynchronized.ref false;
31.9
31.10 fun init false = panic "No Proof General interface support for Isabelle/classic mode."
31.11 | init true =
31.12 @@ -239,9 +239,9 @@
31.13 ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
31.14 setup_thy_loader ();
31.15 setup_present_hook ();
31.16 - set initialized);
31.17 + Unsynchronized.set initialized);
31.18 sync_thy_loader ();
31.19 - change print_mode (update (op =) proof_generalN);
31.20 + Unsynchronized.change print_mode (update (op =) proof_generalN);
31.21 Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
31.22
31.23 end;
32.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 11:48:32 2009 +0200
32.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 29 11:49:22 2009 +0200
32.3 @@ -32,20 +32,20 @@
32.4 (** print mode **)
32.5
32.6 val proof_generalN = "ProofGeneral";
32.7 -val pgmlsymbols_flag = ref true;
32.8 +val pgmlsymbols_flag = Unsynchronized.ref true;
32.9
32.10
32.11 (* assembling and issuing PGIP packets *)
32.12
32.13 -val pgip_refid = ref NONE: string option ref;
32.14 -val pgip_refseq = ref NONE: int option ref;
32.15 +val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
32.16 +val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
32.17
32.18 local
32.19 val pgip_class = "pg"
32.20 val pgip_tag = "Isabelle/Isar"
32.21 - val pgip_id = ref ""
32.22 - val pgip_seq = ref 0
32.23 - fun pgip_serial () = inc pgip_seq
32.24 + val pgip_id = Unsynchronized.ref ""
32.25 + val pgip_seq = Unsynchronized.ref 0
32.26 + fun pgip_serial () = Unsynchronized.inc pgip_seq
32.27
32.28 fun assemble_pgips pgips =
32.29 Pgip { tag = SOME pgip_tag,
32.30 @@ -65,7 +65,7 @@
32.31
32.32 fun matching_pgip_id id = (id = ! pgip_id)
32.33
32.34 -val output_xml_fn = ref Output.writeln_default
32.35 +val output_xml_fn = Unsynchronized.ref Output.writeln_default
32.36 fun output_xml s = ! output_xml_fn (XML.string_of s);
32.37
32.38 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
32.39 @@ -280,7 +280,7 @@
32.40
32.41 (* theorem dependeny output *)
32.42
32.43 -val show_theorem_dependencies = ref false;
32.44 +val show_theorem_dependencies = Unsynchronized.ref false;
32.45
32.46 local
32.47
32.48 @@ -368,13 +368,13 @@
32.49
32.50 (* Preferences: tweak for PGIP interfaces *)
32.51
32.52 -val preferences = ref Preferences.pure_preferences;
32.53 +val preferences = Unsynchronized.ref Preferences.pure_preferences;
32.54
32.55 fun add_preference cat pref =
32.56 - CRITICAL (fn () => change preferences (Preferences.add cat pref));
32.57 + CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
32.58
32.59 fun setup_preferences_tweak () =
32.60 - CRITICAL (fn () => change preferences
32.61 + CRITICAL (fn () => Unsynchronized.change preferences
32.62 (Preferences.set_default ("show-question-marks", "false") #>
32.63 Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
32.64 Preferences.remove "theorem-dependencies" #> (* set internally *)
32.65 @@ -471,7 +471,7 @@
32.66 fun set_proverflag_pgmlsymbols b =
32.67 (pgmlsymbols_flag := b;
32.68 NAMED_CRITICAL "print_mode" (fn () =>
32.69 - change print_mode
32.70 + Unsynchronized.change print_mode
32.71 (fn mode =>
32.72 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
32.73
32.74 @@ -677,7 +677,7 @@
32.75 about this special status, but for now we just keep a local reference.
32.76 *)
32.77
32.78 -val currently_open_file = ref (NONE : pgipurl option)
32.79 +val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
32.80
32.81 fun get_currently_open_file () = ! currently_open_file;
32.82
32.83 @@ -779,7 +779,7 @@
32.84 *)
32.85
32.86 local
32.87 - val current_working_dir = ref (NONE : string option)
32.88 + val current_working_dir = Unsynchronized.ref (NONE : string option)
32.89 in
32.90 fun changecwd_dir newdirpath =
32.91 let
32.92 @@ -1021,7 +1021,7 @@
32.93
32.94 (* init *)
32.95
32.96 -val initialized = ref false;
32.97 +val initialized = Unsynchronized.ref false;
32.98
32.99 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
32.100 | init_pgip true =
32.101 @@ -1035,9 +1035,9 @@
32.102 setup_present_hook ();
32.103 init_pgip_session_id ();
32.104 welcome ();
32.105 - set initialized);
32.106 + Unsynchronized.set initialized);
32.107 sync_thy_loader ();
32.108 - change print_mode (update (op =) proof_generalN);
32.109 + Unsynchronized.change print_mode (update (op =) proof_generalN);
32.110 pgip_toplevel tty_src);
32.111
32.112
32.113 @@ -1045,7 +1045,7 @@
32.114 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
32.115
32.116 local
32.117 - val pgip_output_channel = ref Output.writeln_default
32.118 + val pgip_output_channel = Unsynchronized.ref Output.writeln_default
32.119 in
32.120
32.121 (* Set recipient for PGIP results *)
33.1 --- a/src/Pure/ROOT.ML Tue Sep 29 11:48:32 2009 +0200
33.2 +++ b/src/Pure/ROOT.ML Tue Sep 29 11:49:22 2009 +0200
33.3 @@ -8,7 +8,7 @@
33.4 end;
33.5
33.6 (*if true then some tools will OMIT some proofs*)
33.7 -val quick_and_dirty = ref false;
33.8 +val quick_and_dirty = Unsynchronized.ref false;
33.9
33.10 print_depth 10;
33.11
34.1 --- a/src/Pure/Syntax/ast.ML Tue Sep 29 11:48:32 2009 +0200
34.2 +++ b/src/Pure/Syntax/ast.ML Tue Sep 29 11:49:22 2009 +0200
34.3 @@ -24,8 +24,8 @@
34.4 val fold_ast_p: string -> ast list * ast -> ast
34.5 val unfold_ast: string -> ast -> ast list
34.6 val unfold_ast_p: string -> ast -> ast list * ast
34.7 - val trace_ast: bool ref
34.8 - val stat_ast: bool ref
34.9 + val trace_ast: bool Unsynchronized.ref
34.10 + val stat_ast: bool Unsynchronized.ref
34.11 end;
34.12
34.13 signature AST =
34.14 @@ -173,9 +173,9 @@
34.15
34.16 fun normalize trace stat get_rules pre_ast =
34.17 let
34.18 - val passes = ref 0;
34.19 - val failed_matches = ref 0;
34.20 - val changes = ref 0;
34.21 + val passes = Unsynchronized.ref 0;
34.22 + val failed_matches = Unsynchronized.ref 0;
34.23 + val changes = Unsynchronized.ref 0;
34.24
34.25 fun subst _ (ast as Constant _) = ast
34.26 | subst env (Variable x) = the (Symtab.lookup env x)
34.27 @@ -184,8 +184,8 @@
34.28 fun try_rules ((lhs, rhs) :: pats) ast =
34.29 (case match ast lhs of
34.30 SOME (env, args) =>
34.31 - (inc changes; SOME (mk_appl (subst env rhs) args))
34.32 - | NONE => (inc failed_matches; try_rules pats ast))
34.33 + (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
34.34 + | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
34.35 | try_rules [] _ = NONE;
34.36 val try_headless_rules = try_rules (get_rules "");
34.37
34.38 @@ -226,7 +226,7 @@
34.39 val old_changes = ! changes;
34.40 val new_ast = norm ast;
34.41 in
34.42 - inc passes;
34.43 + Unsynchronized.inc passes;
34.44 if old_changes = ! changes then new_ast else normal new_ast
34.45 end;
34.46
34.47 @@ -245,8 +245,8 @@
34.48
34.49 (* normalize_ast *)
34.50
34.51 -val trace_ast = ref false;
34.52 -val stat_ast = ref false;
34.53 +val trace_ast = Unsynchronized.ref false;
34.54 +val stat_ast = Unsynchronized.ref false;
34.55
34.56 fun normalize_ast get_rules ast =
34.57 normalize (! trace_ast) (! stat_ast) get_rules ast;
35.1 --- a/src/Pure/Syntax/parser.ML Tue Sep 29 11:48:32 2009 +0200
35.2 +++ b/src/Pure/Syntax/parser.ML Tue Sep 29 11:49:22 2009 +0200
35.3 @@ -17,7 +17,7 @@
35.4 Tip of Lexicon.token
35.5 val parse: gram -> string -> Lexicon.token list -> parsetree list
35.6 val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
35.7 - val branching_level: int ref
35.8 + val branching_level: int Unsynchronized.ref
35.9 end;
35.10
35.11 structure Parser: PARSER =
35.12 @@ -690,7 +690,7 @@
35.13 else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
35.14
35.15
35.16 -val branching_level = ref 600; (*trigger value for warnings*)
35.17 +val branching_level = Unsynchronized.ref 600; (*trigger value for warnings*)
35.18
35.19 (*get all productions of a NT and NTs chained to it which can
35.20 be started by specified token*)
35.21 @@ -821,7 +821,7 @@
35.22 val Estate = Array.array (s, []);
35.23 in
35.24 Array.update (Estate, 0, S0);
35.25 - get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
35.26 + get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
35.27 end;
35.28
35.29
36.1 --- a/src/Pure/Syntax/printer.ML Tue Sep 29 11:48:32 2009 +0200
36.2 +++ b/src/Pure/Syntax/printer.ML Tue Sep 29 11:49:22 2009 +0200
36.3 @@ -6,11 +6,11 @@
36.4
36.5 signature PRINTER0 =
36.6 sig
36.7 - val show_brackets: bool ref
36.8 - val show_sorts: bool ref
36.9 - val show_types: bool ref
36.10 - val show_no_free_types: bool ref
36.11 - val show_all_types: bool ref
36.12 + val show_brackets: bool Unsynchronized.ref
36.13 + val show_sorts: bool Unsynchronized.ref
36.14 + val show_types: bool Unsynchronized.ref
36.15 + val show_no_free_types: bool Unsynchronized.ref
36.16 + val show_all_types: bool Unsynchronized.ref
36.17 val pp_show_brackets: Pretty.pp -> Pretty.pp
36.18 end;
36.19
36.20 @@ -42,11 +42,11 @@
36.21
36.22 (** options for printing **)
36.23
36.24 -val show_types = ref false;
36.25 -val show_sorts = ref false;
36.26 -val show_brackets = ref false;
36.27 -val show_no_free_types = ref false;
36.28 -val show_all_types = ref false;
36.29 +val show_types = Unsynchronized.ref false;
36.30 +val show_sorts = Unsynchronized.ref false;
36.31 +val show_brackets = Unsynchronized.ref false;
36.32 +val show_no_free_types = Unsynchronized.ref false;
36.33 +val show_all_types = Unsynchronized.ref false;
36.34
36.35 fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
36.36 Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
37.1 --- a/src/Pure/Syntax/syn_trans.ML Tue Sep 29 11:48:32 2009 +0200
37.2 +++ b/src/Pure/Syntax/syn_trans.ML Tue Sep 29 11:49:22 2009 +0200
37.3 @@ -6,7 +6,7 @@
37.4
37.5 signature SYN_TRANS0 =
37.6 sig
37.7 - val eta_contract: bool ref
37.8 + val eta_contract: bool Unsynchronized.ref
37.9 val atomic_abs_tr': string * typ * term -> term * term
37.10 val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
37.11 val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
37.12 @@ -276,7 +276,7 @@
37.13
37.14 (*do (partial) eta-contraction before printing*)
37.15
37.16 -val eta_contract = ref true;
37.17 +val eta_contract = Unsynchronized.ref true;
37.18
37.19 fun eta_contr tm =
37.20 let
38.1 --- a/src/Pure/Syntax/syntax.ML Tue Sep 29 11:48:32 2009 +0200
38.2 +++ b/src/Pure/Syntax/syntax.ML Tue Sep 29 11:49:22 2009 +0200
38.3 @@ -36,9 +36,9 @@
38.4 val print_syntax: syntax -> unit
38.5 val guess_infix: syntax -> string -> mixfix option
38.6 val read_token: string -> Symbol_Pos.T list * Position.T
38.7 - val ambiguity_is_error: bool ref
38.8 - val ambiguity_level: int ref
38.9 - val ambiguity_limit: int ref
38.10 + val ambiguity_is_error: bool Unsynchronized.ref
38.11 + val ambiguity_level: int Unsynchronized.ref
38.12 + val ambiguity_limit: int Unsynchronized.ref
38.13 val standard_parse_term: Pretty.pp -> (term -> string option) ->
38.14 (((string * int) * sort) list -> string * int -> Term.sort) ->
38.15 (string -> bool * string) -> (string -> string option) ->
38.16 @@ -472,9 +472,9 @@
38.17
38.18 (* read_ast *)
38.19
38.20 -val ambiguity_is_error = ref false;
38.21 -val ambiguity_level = ref 1;
38.22 -val ambiguity_limit = ref 10;
38.23 +val ambiguity_is_error = Unsynchronized.ref false;
38.24 +val ambiguity_level = Unsynchronized.ref 1;
38.25 +val ambiguity_limit = Unsynchronized.ref 10;
38.26
38.27 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
38.28
38.29 @@ -711,7 +711,7 @@
38.30 unparse_typ: Proof.context -> typ -> Pretty.T,
38.31 unparse_term: Proof.context -> term -> Pretty.T};
38.32
38.33 - val operations = ref (NONE: operations option);
38.34 + val operations = Unsynchronized.ref (NONE: operations option);
38.35
38.36 fun operation which ctxt x =
38.37 (case ! operations of
39.1 --- a/src/Pure/System/isabelle_process.ML Tue Sep 29 11:48:32 2009 +0200
39.2 +++ b/src/Pure/System/isabelle_process.ML Tue Sep 29 11:49:22 2009 +0200
39.3 @@ -130,7 +130,7 @@
39.4 (* init *)
39.5
39.6 fun init out =
39.7 - (change print_mode (update (op =) isabelle_processN);
39.8 + (Unsynchronized.change print_mode (update (op =) isabelle_processN);
39.9 setup_channels out |> init_message;
39.10 OuterKeyword.report ();
39.11 Output.status (Markup.markup Markup.ready "");
40.1 --- a/src/Pure/System/isar.ML Tue Sep 29 11:48:32 2009 +0200
40.2 +++ b/src/Pure/System/isar.ML Tue Sep 29 11:49:22 2009 +0200
40.3 @@ -18,7 +18,7 @@
40.4 val undo: int -> unit
40.5 val kill: unit -> unit
40.6 val kill_proof: unit -> unit
40.7 - val crashes: exn list ref
40.8 + val crashes: exn list Unsynchronized.ref
40.9 val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
40.10 val loop: unit -> unit
40.11 val main: unit -> unit
40.12 @@ -36,9 +36,9 @@
40.13 (*previous state, state transition -- regular commands only*)
40.14
40.15 local
40.16 - val global_history = ref ([]: history);
40.17 - val global_state = ref Toplevel.toplevel;
40.18 - val global_exn = ref (NONE: (exn * string) option);
40.19 + val global_history = Unsynchronized.ref ([]: history);
40.20 + val global_state = Unsynchronized.ref Toplevel.toplevel;
40.21 + val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
40.22 in
40.23
40.24 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
40.25 @@ -115,7 +115,7 @@
40.26
40.27 (* toplevel loop *)
40.28
40.29 -val crashes = ref ([]: exn list);
40.30 +val crashes = Unsynchronized.ref ([]: exn list);
40.31
40.32 local
40.33
40.34 @@ -130,7 +130,7 @@
40.35 handle exn =>
40.36 (Output.error_msg (ML_Compiler.exn_message exn)
40.37 handle crash =>
40.38 - (CRITICAL (fn () => change crashes (cons crash));
40.39 + (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
40.40 warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
40.41 raw_loop secure src)
40.42 end;
41.1 --- a/src/Pure/System/session.ML Tue Sep 29 11:48:32 2009 +0200
41.2 +++ b/src/Pure/System/session.ML Tue Sep 29 11:49:22 2009 +0200
41.3 @@ -21,10 +21,10 @@
41.4
41.5 (* session state *)
41.6
41.7 -val session = ref ([Context.PureN]: string list);
41.8 -val session_path = ref ([]: string list);
41.9 -val session_finished = ref false;
41.10 -val remote_path = ref (NONE: Url.T option);
41.11 +val session = Unsynchronized.ref ([Context.PureN]: string list);
41.12 +val session_path = Unsynchronized.ref ([]: string list);
41.13 +val session_finished = Unsynchronized.ref false;
41.14 +val remote_path = Unsynchronized.ref (NONE: Url.T option);
41.15
41.16
41.17 (* access path *)
42.1 --- a/src/Pure/Thy/html.ML Tue Sep 29 11:48:32 2009 +0200
42.2 +++ b/src/Pure/Thy/html.ML Tue Sep 29 11:49:22 2009 +0200
42.3 @@ -267,8 +267,8 @@
42.4
42.5 (* document *)
42.6
42.7 -val charset = ref "ISO-8859-1";
42.8 -fun with_charset s = setmp_noncritical charset s;
42.9 +val charset = Unsynchronized.ref "ISO-8859-1";
42.10 +fun with_charset s = setmp_noncritical charset s; (* FIXME *)
42.11
42.12 fun begin_document title =
42.13 let val cs = ! charset in
43.1 --- a/src/Pure/Thy/present.ML Tue Sep 29 11:48:32 2009 +0200
43.2 +++ b/src/Pure/Thy/present.ML Tue Sep 29 11:49:22 2009 +0200
43.3 @@ -161,10 +161,11 @@
43.4
43.5 (* state *)
43.6
43.7 -val browser_info = ref empty_browser_info;
43.8 -fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
43.9 +val browser_info = Unsynchronized.ref empty_browser_info;
43.10 +fun change_browser_info f =
43.11 + CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
43.12
43.13 -val suppress_tex_source = ref false;
43.14 +val suppress_tex_source = Unsynchronized.ref false;
43.15 fun no_document f x = setmp_noncritical suppress_tex_source true f x;
43.16
43.17 fun init_theory_info name info =
43.18 @@ -229,7 +230,7 @@
43.19
43.20 (* state *)
43.21
43.22 -val session_info = ref (NONE: session_info option);
43.23 +val session_info = Unsynchronized.ref (NONE: session_info option);
43.24
43.25 fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
43.26 fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
43.27 @@ -534,5 +535,5 @@
43.28
43.29 end;
43.30
43.31 -structure BasicPresent: BASIC_PRESENT = Present;
43.32 -open BasicPresent;
43.33 +structure Basic_Present: BASIC_PRESENT = Present;
43.34 +open Basic_Present;
44.1 --- a/src/Pure/Thy/thy_info.ML Tue Sep 29 11:48:32 2009 +0200
44.2 +++ b/src/Pure/Thy/thy_info.ML Tue Sep 29 11:49:22 2009 +0200
44.3 @@ -50,9 +50,9 @@
44.4 val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
44.5
44.6 local
44.7 - val hooks = ref ([]: (action -> string -> unit) list);
44.8 + val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
44.9 in
44.10 - fun add_hook f = CRITICAL (fn () => change hooks (cons f));
44.11 + fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
44.12 fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
44.13 end;
44.14
44.15 @@ -111,10 +111,10 @@
44.16 type thy = deps option * theory option;
44.17
44.18 local
44.19 - val database = ref (Graph.empty: thy Graph.T);
44.20 + val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
44.21 in
44.22 fun get_thys () = ! database;
44.23 - fun change_thys f = CRITICAL (fn () => Library.change database f);
44.24 + fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
44.25 end;
44.26
44.27
45.1 --- a/src/Pure/Thy/thy_load.ML Tue Sep 29 11:48:32 2009 +0200
45.2 +++ b/src/Pure/Thy/thy_load.ML Tue Sep 29 11:49:22 2009 +0200
45.3 @@ -37,14 +37,16 @@
45.4
45.5 (* maintain load path *)
45.6
45.7 -local val load_path = ref [Path.current] in
45.8 +local val load_path = Unsynchronized.ref [Path.current] in
45.9
45.10 fun show_path () = map Path.implode (! load_path);
45.11
45.12 -fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
45.13 -fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
45.14 -fun path_add s =
45.15 - CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
45.16 +fun del_path s = CRITICAL (fn () =>
45.17 + Unsynchronized.change load_path (remove (op =) (Path.explode s)));
45.18 +fun add_path s = CRITICAL (fn () =>
45.19 + (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
45.20 +fun path_add s = CRITICAL (fn () =>
45.21 + (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
45.22 fun reset_path () = load_path := [Path.current];
45.23
45.24 fun with_paths ss f x =
45.25 @@ -124,5 +126,5 @@
45.26
45.27 end;
45.28
45.29 -structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
45.30 -open BasicThyLoad;
45.31 +structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
45.32 +open Basic_Thy_Load;
46.1 --- a/src/Pure/Thy/thy_output.ML Tue Sep 29 11:48:32 2009 +0200
46.2 +++ b/src/Pure/Thy/thy_output.ML Tue Sep 29 11:49:22 2009 +0200
46.3 @@ -6,11 +6,11 @@
46.4
46.5 signature THY_OUTPUT =
46.6 sig
46.7 - val display: bool ref
46.8 - val quotes: bool ref
46.9 - val indent: int ref
46.10 - val source: bool ref
46.11 - val break: bool ref
46.12 + val display: bool Unsynchronized.ref
46.13 + val quotes: bool Unsynchronized.ref
46.14 + val indent: int Unsynchronized.ref
46.15 + val source: bool Unsynchronized.ref
46.16 + val break: bool Unsynchronized.ref
46.17 val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
46.18 val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
46.19 val defined_command: string -> bool
46.20 @@ -21,7 +21,7 @@
46.21 val antiquotation: string -> 'a context_parser ->
46.22 ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
46.23 datatype markup = Markup | MarkupEnv | Verbatim
46.24 - val modes: string list ref
46.25 + val modes: string list Unsynchronized.ref
46.26 val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
46.27 val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
46.28 (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
46.29 @@ -42,11 +42,11 @@
46.30
46.31 (** global options **)
46.32
46.33 -val display = ref false;
46.34 -val quotes = ref false;
46.35 -val indent = ref 0;
46.36 -val source = ref false;
46.37 -val break = ref false;
46.38 +val display = Unsynchronized.ref false;
46.39 +val quotes = Unsynchronized.ref false;
46.40 +val indent = Unsynchronized.ref 0;
46.41 +val source = Unsynchronized.ref false;
46.42 +val break = Unsynchronized.ref false;
46.43
46.44
46.45
46.46 @@ -55,10 +55,10 @@
46.47 local
46.48
46.49 val global_commands =
46.50 - ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
46.51 + Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
46.52
46.53 val global_options =
46.54 - ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
46.55 + Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
46.56
46.57 fun add_item kind (name, x) tab =
46.58 (if not (Symtab.defined tab name) then ()
46.59 @@ -67,8 +67,10 @@
46.60
46.61 in
46.62
46.63 -fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
46.64 -fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
46.65 +fun add_commands xs =
46.66 + CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
46.67 +fun add_options xs =
46.68 + CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
46.69
46.70 fun defined_command name = Symtab.defined (! global_commands) name;
46.71 fun defined_option name = Symtab.defined (! global_options) name;
46.72 @@ -143,7 +145,7 @@
46.73
46.74 (* eval_antiquote *)
46.75
46.76 -val modes = ref ([]: string list);
46.77 +val modes = Unsynchronized.ref ([]: string list);
46.78
46.79 fun eval_antiquote lex state (txt, pos) =
46.80 let
47.1 --- a/src/Pure/Tools/find_theorems.ML Tue Sep 29 11:48:32 2009 +0200
47.2 +++ b/src/Pure/Tools/find_theorems.ML Tue Sep 29 11:49:22 2009 +0200
47.3 @@ -9,8 +9,8 @@
47.4 datatype 'term criterion =
47.5 Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
47.6 Pattern of 'term
47.7 - val tac_limit: int ref
47.8 - val limit: int ref
47.9 + val tac_limit: int Unsynchronized.ref
47.10 + val limit: int Unsynchronized.ref
47.11 val find_theorems: Proof.context -> thm option -> int option -> bool ->
47.12 (bool * string criterion) list -> int option * (Facts.ref * thm) list
47.13 val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
47.14 @@ -186,7 +186,7 @@
47.15 end
47.16 else NONE
47.17
47.18 -val tac_limit = ref 5;
47.19 +val tac_limit = Unsynchronized.ref 5;
47.20
47.21 fun filter_solves ctxt goal =
47.22 let
47.23 @@ -372,7 +372,7 @@
47.24 (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
47.25 Facts.dest_static [] (ProofContext.facts_of ctxt));
47.26
47.27 -val limit = ref 40;
47.28 +val limit = Unsynchronized.ref 40;
47.29
47.30 fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
47.31 let
48.1 --- a/src/Pure/codegen.ML Tue Sep 29 11:48:32 2009 +0200
48.2 +++ b/src/Pure/codegen.ML Tue Sep 29 11:49:22 2009 +0200
48.3 @@ -6,10 +6,10 @@
48.4
48.5 signature CODEGEN =
48.6 sig
48.7 - val quiet_mode : bool ref
48.8 + val quiet_mode : bool Unsynchronized.ref
48.9 val message : string -> unit
48.10 - val mode : string list ref
48.11 - val margin : int ref
48.12 + val mode : string list Unsynchronized.ref
48.13 + val margin : int Unsynchronized.ref
48.14 val string_of : Pretty.T -> string
48.15 val str : string -> Pretty.T
48.16
48.17 @@ -75,9 +75,9 @@
48.18 val mk_type: bool -> typ -> Pretty.T
48.19 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
48.20 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
48.21 - val test_fn: (int -> term list option) ref
48.22 + val test_fn: (int -> term list option) Unsynchronized.ref
48.23 val test_term: Proof.context -> term -> int -> term list option
48.24 - val eval_result: (unit -> term) ref
48.25 + val eval_result: (unit -> term) Unsynchronized.ref
48.26 val eval_term: theory -> term -> term
48.27 val evaluation_conv: cterm -> thm
48.28 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
48.29 @@ -102,12 +102,12 @@
48.30 structure Codegen : CODEGEN =
48.31 struct
48.32
48.33 -val quiet_mode = ref true;
48.34 +val quiet_mode = Unsynchronized.ref true;
48.35 fun message s = if !quiet_mode then () else writeln s;
48.36
48.37 -val mode = ref ([] : string list);
48.38 +val mode = Unsynchronized.ref ([] : string list);
48.39
48.40 -val margin = ref 80;
48.41 +val margin = Unsynchronized.ref 80;
48.42
48.43 fun string_of p = (Pretty.string_of |>
48.44 PrintMode.setmp [] |>
48.45 @@ -878,7 +878,8 @@
48.46 [mk_gen gr module true xs a T, mk_type true T]) Ts) @
48.47 (if member (op =) xs s then [str a] else []))));
48.48
48.49 -val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
48.50 +val test_fn : (int -> term list option) Unsynchronized.ref =
48.51 + Unsynchronized.ref (fn _ => NONE);
48.52
48.53 fun test_term ctxt t =
48.54 let
48.55 @@ -912,7 +913,7 @@
48.56
48.57 (**** Evaluator for terms ****)
48.58
48.59 -val eval_result = ref (fn () => Bound 0);
48.60 +val eval_result = Unsynchronized.ref (fn () => Bound 0);
48.61
48.62 fun eval_term thy t =
48.63 let
49.1 --- a/src/Pure/context.ML Tue Sep 29 11:48:32 2009 +0200
49.2 +++ b/src/Pure/context.ML Tue Sep 29 11:49:22 2009 +0200
49.3 @@ -107,7 +107,7 @@
49.4 extend: Object.T -> Object.T,
49.5 merge: Pretty.pp -> Object.T * Object.T -> Object.T};
49.6
49.7 -val kinds = ref (Datatab.empty: kind Datatab.table);
49.8 +val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
49.9
49.10 fun invoke f k =
49.11 (case Datatab.lookup (! kinds) k of
49.12 @@ -125,7 +125,7 @@
49.13 let
49.14 val k = serial ();
49.15 val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
49.16 - val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
49.17 + val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
49.18 in k end;
49.19
49.20 val copy_data = Datatab.map' invoke_copy;
49.21 @@ -149,7 +149,7 @@
49.22 datatype theory =
49.23 Theory of
49.24 (*identity*)
49.25 - {self: theory ref option, (*dynamic self reference -- follows theory changes*)
49.26 + {self: theory Unsynchronized.ref option, (*dynamic self reference -- follows theory changes*)
49.27 draft: bool, (*draft mode -- linear destructive changes*)
49.28 id: serial, (*identifier*)
49.29 ids: unit Inttab.table} * (*cumulative identifiers of non-drafts -- symbolic body content*)
49.30 @@ -186,14 +186,15 @@
49.31 fun eq_id (i: int, j) = i = j;
49.32
49.33 fun is_stale
49.34 - (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
49.35 + (Theory ({self =
49.36 + SOME (Unsynchronized.ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
49.37 not (eq_id (id, id'))
49.38 | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
49.39
49.40 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
49.41 | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
49.42 let
49.43 - val r = ref thy;
49.44 + val r = Unsynchronized.ref thy;
49.45 val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
49.46 in r := thy'; thy' end;
49.47
49.48 @@ -243,9 +244,9 @@
49.49 theory in external data structures -- a plain theory value would
49.50 become stale as the self reference moves on*)
49.51
49.52 -datatype theory_ref = TheoryRef of theory ref;
49.53 +datatype theory_ref = TheoryRef of theory Unsynchronized.ref;
49.54
49.55 -fun deref (TheoryRef (ref thy)) = thy;
49.56 +fun deref (TheoryRef (Unsynchronized.ref thy)) = thy;
49.57
49.58 fun check_thy thy = (*thread-safe version*)
49.59 let val thy_ref = TheoryRef (the_self thy) in
49.60 @@ -437,7 +438,7 @@
49.61
49.62 local
49.63
49.64 -val kinds = ref (Datatab.empty: (theory -> Object.T) Datatab.table);
49.65 +val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
49.66
49.67 fun invoke_init k =
49.68 (case Datatab.lookup (! kinds) k of
49.69 @@ -470,7 +471,7 @@
49.70 fun declare init =
49.71 let
49.72 val k = serial ();
49.73 - val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
49.74 + val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
49.75 in k end;
49.76
49.77 fun get k dest prf =
50.1 --- a/src/Pure/display.ML Tue Sep 29 11:48:32 2009 +0200
50.2 +++ b/src/Pure/display.ML Tue Sep 29 11:49:22 2009 +0200
50.3 @@ -7,10 +7,10 @@
50.4
50.5 signature BASIC_DISPLAY =
50.6 sig
50.7 - val goals_limit: int ref
50.8 - val show_consts: bool ref
50.9 - val show_hyps: bool ref
50.10 - val show_tags: bool ref
50.11 + val goals_limit: int Unsynchronized.ref
50.12 + val show_consts: bool Unsynchronized.ref
50.13 + val show_hyps: bool Unsynchronized.ref
50.14 + val show_tags: bool Unsynchronized.ref
50.15 end;
50.16
50.17 signature DISPLAY =
50.18 @@ -39,8 +39,8 @@
50.19 val goals_limit = Goal_Display.goals_limit;
50.20 val show_consts = Goal_Display.show_consts;
50.21
50.22 -val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
50.23 -val show_tags = ref false; (*false: suppress tags*)
50.24 +val show_hyps = Unsynchronized.ref false; (*false: print meta-hypotheses as dots*)
50.25 +val show_tags = Unsynchronized.ref false; (*false: suppress tags*)
50.26
50.27
50.28
51.1 --- a/src/Pure/goal.ML Tue Sep 29 11:48:32 2009 +0200
51.2 +++ b/src/Pure/goal.ML Tue Sep 29 11:49:22 2009 +0200
51.3 @@ -6,7 +6,7 @@
51.4
51.5 signature BASIC_GOAL =
51.6 sig
51.7 - val parallel_proofs: int ref
51.8 + val parallel_proofs: int Unsynchronized.ref
51.9 val SELECT_GOAL: tactic -> int -> tactic
51.10 val CONJUNCTS: tactic -> int -> tactic
51.11 val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
51.12 @@ -102,7 +102,7 @@
51.13
51.14 (* future_enabled *)
51.15
51.16 -val parallel_proofs = ref 1;
51.17 +val parallel_proofs = Unsynchronized.ref 1;
51.18
51.19 fun future_enabled () =
51.20 Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
52.1 --- a/src/Pure/goal_display.ML Tue Sep 29 11:48:32 2009 +0200
52.2 +++ b/src/Pure/goal_display.ML Tue Sep 29 11:49:22 2009 +0200
52.3 @@ -7,8 +7,8 @@
52.4
52.5 signature GOAL_DISPLAY =
52.6 sig
52.7 - val goals_limit: int ref
52.8 - val show_consts: bool ref
52.9 + val goals_limit: int Unsynchronized.ref
52.10 + val show_consts: bool Unsynchronized.ref
52.11 val pretty_flexpair: Proof.context -> term * term -> Pretty.T
52.12 val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
52.13 thm -> Pretty.T list
52.14 @@ -18,8 +18,8 @@
52.15 structure Goal_Display: GOAL_DISPLAY =
52.16 struct
52.17
52.18 -val goals_limit = ref 10; (*max number of goals to print*)
52.19 -val show_consts = ref false; (*true: show consts with types in proof state output*)
52.20 +val goals_limit = Unsynchronized.ref 10; (*max number of goals to print*)
52.21 +val show_consts = Unsynchronized.ref false; (*true: show consts with types in proof state output*)
52.22
52.23 fun pretty_flexpair ctxt (t, u) = Pretty.block
52.24 [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
53.1 --- a/src/Pure/meta_simplifier.ML Tue Sep 29 11:48:32 2009 +0200
53.2 +++ b/src/Pure/meta_simplifier.ML Tue Sep 29 11:49:22 2009 +0200
53.3 @@ -11,9 +11,9 @@
53.4
53.5 signature BASIC_META_SIMPLIFIER =
53.6 sig
53.7 - val debug_simp: bool ref
53.8 - val trace_simp: bool ref
53.9 - val trace_simp_depth_limit: int ref
53.10 + val debug_simp: bool Unsynchronized.ref
53.11 + val trace_simp: bool Unsynchronized.ref
53.12 + val trace_simp_depth_limit: int Unsynchronized.ref
53.13 type rrule
53.14 val eq_rrule: rrule * rrule -> bool
53.15 type simpset
53.16 @@ -84,7 +84,7 @@
53.17 {rules: rrule Net.net,
53.18 prems: thm list,
53.19 bounds: int * ((string * typ) * string) list,
53.20 - depth: int * bool ref,
53.21 + depth: int * bool Unsynchronized.ref,
53.22 context: Proof.context option} *
53.23 {congs: (string * thm) list * string list,
53.24 procs: proc Net.net,
53.25 @@ -112,7 +112,7 @@
53.26 val the_context: simpset -> Proof.context
53.27 val context: Proof.context -> simpset -> simpset
53.28 val theory_context: theory -> simpset -> simpset
53.29 - val debug_bounds: bool ref
53.30 + val debug_bounds: bool Unsynchronized.ref
53.31 val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
53.32 val set_solvers: solver list -> simpset -> simpset
53.33 val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
53.34 @@ -190,7 +190,7 @@
53.35 {rules: rrule Net.net,
53.36 prems: thm list,
53.37 bounds: int * ((string * typ) * string) list,
53.38 - depth: int * bool ref,
53.39 + depth: int * bool Unsynchronized.ref,
53.40 context: Proof.context option} *
53.41 {congs: (string * thm) list * string list,
53.42 procs: proc Net.net,
53.43 @@ -256,7 +256,7 @@
53.44 val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
53.45 val simp_depth_limit = Config.int simp_depth_limit_value;
53.46
53.47 -val trace_simp_depth_limit = ref 1;
53.48 +val trace_simp_depth_limit = Unsynchronized.ref 1;
53.49
53.50 fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
53.51 if depth > ! trace_simp_depth_limit then
53.52 @@ -266,7 +266,8 @@
53.53
53.54 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
53.55 (rules, prems, bounds,
53.56 - (depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
53.57 + (depth + 1,
53.58 + if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
53.59
53.60 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
53.61
53.62 @@ -275,8 +276,8 @@
53.63
53.64 exception SIMPLIFIER of string * thm;
53.65
53.66 -val debug_simp = ref false;
53.67 -val trace_simp = ref false;
53.68 +val debug_simp = Unsynchronized.ref false;
53.69 +val trace_simp = Unsynchronized.ref false;
53.70
53.71 local
53.72
53.73 @@ -746,7 +747,7 @@
53.74 (* empty *)
53.75
53.76 fun init_ss mk_rews termless subgoal_tac solvers =
53.77 - make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
53.78 + make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
53.79 (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
53.80
53.81 fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
53.82 @@ -1209,7 +1210,7 @@
53.83 prover: how to solve premises in conditional rewrites and congruences
53.84 *)
53.85
53.86 -val debug_bounds = ref false;
53.87 +val debug_bounds = Unsynchronized.ref false;
53.88
53.89 fun check_bounds ss ct =
53.90 if ! debug_bounds then
53.91 @@ -1337,5 +1338,5 @@
53.92
53.93 end;
53.94
53.95 -structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
53.96 -open BasicMetaSimplifier;
53.97 +structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
53.98 +open Basic_Meta_Simplifier;
54.1 --- a/src/Pure/old_goals.ML Tue Sep 29 11:48:32 2009 +0200
54.2 +++ b/src/Pure/old_goals.ML Tue Sep 29 11:49:22 2009 +0200
54.3 @@ -19,7 +19,7 @@
54.4 type proof
54.5 val premises: unit -> thm list
54.6 val reset_goals: unit -> unit
54.7 - val result_error_fn: (thm -> string -> thm) ref
54.8 + val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
54.9 val print_sign_exn: theory -> exn -> 'a
54.10 val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
54.11 val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
54.12 @@ -233,21 +233,21 @@
54.13 (*** References ***)
54.14
54.15 (*Current assumption list -- set by "goal".*)
54.16 -val curr_prems = ref([] : thm list);
54.17 +val curr_prems = Unsynchronized.ref([] : thm list);
54.18
54.19 (*Return assumption list -- useful if you didn't save "goal"'s result. *)
54.20 fun premises() = !curr_prems;
54.21
54.22 (*Current result maker -- set by "goal", used by "result". *)
54.23 fun init_mkresult _ = error "No goal has been supplied in subgoal module";
54.24 -val curr_mkresult = ref (init_mkresult: bool*thm->thm);
54.25 +val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
54.26
54.27 (*List of previous goal stacks, for the undo operation. Set by setstate.
54.28 A list of lists!*)
54.29 -val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
54.30 +val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
54.31
54.32 (* Stack of proof attempts *)
54.33 -val proofstack = ref([]: proof list);
54.34 +val proofstack = Unsynchronized.ref([]: proof list);
54.35
54.36 (*reset all refs*)
54.37 fun reset_goals () =
54.38 @@ -272,7 +272,7 @@
54.39 Goal_Display.pretty_goals_without_context (!goals_limit) state @
54.40 [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
54.41
54.42 -val result_error_fn = ref result_error_default;
54.43 +val result_error_fn = Unsynchronized.ref result_error_default;
54.44
54.45
54.46 (*Common treatment of "goal" and "prove_goal":
55.1 --- a/src/Pure/pattern.ML Tue Sep 29 11:48:32 2009 +0200
55.2 +++ b/src/Pure/pattern.ML Tue Sep 29 11:49:22 2009 +0200
55.3 @@ -14,7 +14,7 @@
55.4
55.5 signature PATTERN =
55.6 sig
55.7 - val trace_unify_fail: bool ref
55.8 + val trace_unify_fail: bool Unsynchronized.ref
55.9 val aeconv: term * term -> bool
55.10 val eta_long: typ list -> term -> term
55.11 val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
55.12 @@ -40,7 +40,7 @@
55.13 exception Unif;
55.14 exception Pattern;
55.15
55.16 -val trace_unify_fail = ref false;
55.17 +val trace_unify_fail = Unsynchronized.ref false;
55.18
55.19 fun string_of_term thy env binders t =
55.20 Syntax.string_of_term_global thy
56.1 --- a/src/Pure/proofterm.ML Tue Sep 29 11:48:32 2009 +0200
56.2 +++ b/src/Pure/proofterm.ML Tue Sep 29 11:49:22 2009 +0200
56.3 @@ -8,7 +8,7 @@
56.4
56.5 signature BASIC_PROOFTERM =
56.6 sig
56.7 - val proofs: int ref
56.8 + val proofs: int Unsynchronized.ref
56.9
56.10 datatype proof =
56.11 MinProof
56.12 @@ -885,7 +885,7 @@
56.13
56.14 (***** axioms and theorems *****)
56.15
56.16 -val proofs = ref 2;
56.17 +val proofs = Unsynchronized.ref 2;
56.18
56.19 fun vars_of t = map Var (rev (Term.add_vars t []));
56.20 fun frees_of t = map Free (rev (Term.add_frees t []));
57.1 --- a/src/Pure/search.ML Tue Sep 29 11:48:32 2009 +0200
57.2 +++ b/src/Pure/search.ML Tue Sep 29 11:49:22 2009 +0200
57.3 @@ -13,23 +13,23 @@
57.4 val THEN_MAYBE : tactic * tactic -> tactic
57.5 val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
57.6
57.7 - val trace_DEPTH_FIRST : bool ref
57.8 + val trace_DEPTH_FIRST : bool Unsynchronized.ref
57.9 val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
57.10 val DEPTH_SOLVE : tactic -> tactic
57.11 val DEPTH_SOLVE_1 : tactic -> tactic
57.12 val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
57.13 val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
57.14 - val iter_deepen_limit : int ref
57.15 + val iter_deepen_limit : int Unsynchronized.ref
57.16
57.17 val has_fewer_prems : int -> thm -> bool
57.18 val IF_UNSOLVED : tactic -> tactic
57.19 val SOLVE : tactic -> tactic
57.20 val DETERM_UNTIL_SOLVED: tactic -> tactic
57.21 - val trace_BEST_FIRST : bool ref
57.22 + val trace_BEST_FIRST : bool Unsynchronized.ref
57.23 val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
57.24 val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
57.25 -> tactic
57.26 - val trace_ASTAR : bool ref
57.27 + val trace_ASTAR : bool Unsynchronized.ref
57.28 val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
57.29 val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
57.30 -> tactic
57.31 @@ -50,7 +50,7 @@
57.32
57.33 (**** Depth-first search ****)
57.34
57.35 -val trace_DEPTH_FIRST = ref false;
57.36 +val trace_DEPTH_FIRST = Unsynchronized.ref false;
57.37
57.38 (*Searches until "satp" reports proof tree as satisfied.
57.39 Suppresses duplicate solutions to minimize search space.*)
57.40 @@ -130,7 +130,7 @@
57.41
57.42
57.43 (*No known example (on 1-5-2007) needs even thirty*)
57.44 -val iter_deepen_limit = ref 50;
57.45 +val iter_deepen_limit = Unsynchronized.ref 50;
57.46
57.47 (*Depth-first iterative deepening search for a state that satisfies satp
57.48 tactic tac0 sets up the initial goal queue, while tac1 searches it.
57.49 @@ -138,7 +138,7 @@
57.50 to suppress solutions arising from earlier searches, as the accumulated cost
57.51 (k) can be wrong.*)
57.52 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
57.53 - let val countr = ref 0
57.54 + let val countr = Unsynchronized.ref 0
57.55 and tf = tracify trace_DEPTH_FIRST (tac1 1)
57.56 and qs0 = tac0 st
57.57 (*bnd = depth bound; inc = estimate of increment required next*)
57.58 @@ -156,7 +156,7 @@
57.59 | depth (bnd,inc) ((k,np,rgd,q)::qs) =
57.60 if k>=bnd then depth (bnd,inc) qs
57.61 else
57.62 - case (countr := !countr+1;
57.63 + case (Unsynchronized.inc countr;
57.64 if !trace_DEPTH_FIRST then
57.65 tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
57.66 else ();
57.67 @@ -199,7 +199,7 @@
57.68
57.69 (*** Best-first search ***)
57.70
57.71 -val trace_BEST_FIRST = ref false;
57.72 +val trace_BEST_FIRST = Unsynchronized.ref false;
57.73
57.74 (*For creating output sequence*)
57.75 fun some_of_list [] = NONE
57.76 @@ -273,7 +273,7 @@
57.77 fun some_of_list [] = NONE
57.78 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
57.79
57.80 -val trace_ASTAR = ref false;
57.81 +val trace_ASTAR = Unsynchronized.ref false;
57.82
57.83 fun THEN_ASTAR tac0 (satp, costf) tac1 =
57.84 let val tf = tracify trace_ASTAR tac1;
58.1 --- a/src/Pure/simplifier.ML Tue Sep 29 11:48:32 2009 +0200
58.2 +++ b/src/Pure/simplifier.ML Tue Sep 29 11:49:22 2009 +0200
58.3 @@ -32,7 +32,7 @@
58.4 include BASIC_SIMPLIFIER
58.5 val pretty_ss: Proof.context -> simpset -> Pretty.T
58.6 val clear_ss: simpset -> simpset
58.7 - val debug_bounds: bool ref
58.8 + val debug_bounds: bool Unsynchronized.ref
58.9 val inherit_context: simpset -> simpset -> simpset
58.10 val the_context: simpset -> Proof.context
58.11 val context: Proof.context -> simpset -> simpset
58.12 @@ -424,5 +424,5 @@
58.13
58.14 end;
58.15
58.16 -structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
58.17 -open BasicSimplifier;
58.18 +structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
58.19 +open Basic_Simplifier;
59.1 --- a/src/Pure/tactical.ML Tue Sep 29 11:48:32 2009 +0200
59.2 +++ b/src/Pure/tactical.ML Tue Sep 29 11:49:22 2009 +0200
59.3 @@ -34,9 +34,9 @@
59.4 val RANGE: (int -> tactic) list -> int -> tactic
59.5 val print_tac: string -> tactic
59.6 val pause_tac: tactic
59.7 - val trace_REPEAT: bool ref
59.8 - val suppress_tracing: bool ref
59.9 - val tracify: bool ref -> tactic -> tactic
59.10 + val trace_REPEAT: bool Unsynchronized.ref
59.11 + val suppress_tracing: bool Unsynchronized.ref
59.12 + val tracify: bool Unsynchronized.ref -> tactic -> tactic
59.13 val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
59.14 val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
59.15 val REPEAT_DETERM_N: int -> tactic -> tactic
59.16 @@ -204,16 +204,16 @@
59.17 and TRACE_QUIT;
59.18
59.19 (*Tracing flags*)
59.20 -val trace_REPEAT= ref false
59.21 -and suppress_tracing = ref false;
59.22 +val trace_REPEAT= Unsynchronized.ref false
59.23 +and suppress_tracing = Unsynchronized.ref false;
59.24
59.25 (*Handle all tracing commands for current state and tactic *)
59.26 fun exec_trace_command flag (tac, st) =
59.27 case TextIO.inputLine TextIO.stdIn of
59.28 SOME "\n" => tac st
59.29 | SOME "f\n" => Seq.empty
59.30 - | SOME "o\n" => (flag:=false; tac st)
59.31 - | SOME "s\n" => (suppress_tracing:=true; tac st)
59.32 + | SOME "o\n" => (flag := false; tac st)
59.33 + | SOME "s\n" => (suppress_tracing := true; tac st)
59.34 | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
59.35 | SOME "quit\n" => raise TRACE_QUIT
59.36 | _ => (tracing
60.1 --- a/src/Pure/term.ML Tue Sep 29 11:48:32 2009 +0200
60.2 +++ b/src/Pure/term.ML Tue Sep 29 11:49:22 2009 +0200
60.3 @@ -112,7 +112,7 @@
60.4 val exists_type: (typ -> bool) -> term -> bool
60.5 val exists_subterm: (term -> bool) -> term -> bool
60.6 val exists_Const: (string * typ -> bool) -> term -> bool
60.7 - val show_question_marks: bool ref
60.8 + val show_question_marks: bool Unsynchronized.ref
60.9 end;
60.10
60.11 signature TERM =
60.12 @@ -963,7 +963,7 @@
60.13
60.14 (* display variables *)
60.15
60.16 -val show_question_marks = ref true;
60.17 +val show_question_marks = Unsynchronized.ref true;
60.18
60.19 fun string_of_vname (x, i) =
60.20 let
61.1 --- a/src/Pure/term_subst.ML Tue Sep 29 11:48:32 2009 +0200
61.2 +++ b/src/Pure/term_subst.ML Tue Sep 29 11:49:22 2009 +0200
61.3 @@ -157,28 +157,32 @@
61.4 in
61.5
61.6 fun instantiateT_maxidx instT ty i =
61.7 - let val maxidx = ref i
61.8 + let val maxidx = Unsynchronized.ref i
61.9 in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
61.10
61.11 fun instantiate_maxidx insts tm i =
61.12 - let val maxidx = ref i
61.13 + let val maxidx = Unsynchronized.ref i
61.14 in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
61.15
61.16 fun instantiateT [] ty = ty
61.17 | instantiateT instT ty =
61.18 - (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
61.19 + (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
61.20 + handle Same.SAME => ty);
61.21
61.22 fun instantiate ([], []) tm = tm
61.23 | instantiate insts tm =
61.24 - (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
61.25 + (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
61.26 + handle Same.SAME => tm);
61.27
61.28 fun instantiateT_option [] _ = NONE
61.29 | instantiateT_option instT ty =
61.30 - (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
61.31 + (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
61.32 + handle Same.SAME => NONE);
61.33
61.34 fun instantiate_option ([], []) _ = NONE
61.35 | instantiate_option insts tm =
61.36 - (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
61.37 + (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
61.38 + handle Same.SAME => NONE);
61.39
61.40 end;
61.41
62.1 --- a/src/Pure/type.ML Tue Sep 29 11:48:32 2009 +0200
62.2 +++ b/src/Pure/type.ML Tue Sep 29 11:49:22 2009 +0200
62.3 @@ -417,8 +417,8 @@
62.4 (*order-sorted unification*)
62.5 fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
62.6 let
62.7 - val tyvar_count = ref maxidx;
62.8 - fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
62.9 + val tyvar_count = Unsynchronized.ref maxidx;
62.10 + fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
62.11
62.12 fun mg_domain a S = Sorts.mg_domain classes a S
62.13 handle Sorts.CLASS_ERROR _ => raise TUNIFY;
63.1 --- a/src/Pure/unify.ML Tue Sep 29 11:48:32 2009 +0200
63.2 +++ b/src/Pure/unify.ML Tue Sep 29 11:49:22 2009 +0200
63.3 @@ -106,7 +106,7 @@
63.4 the occurs check must ignore the types of variables. This avoids
63.5 that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
63.6 substitution when ?'a is instantiated with T later. *)
63.7 -fun occurs_terms (seen: (indexname list) ref,
63.8 +fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
63.9 env: Envir.env, v: indexname, ts: term list): bool =
63.10 let fun occurs [] = false
63.11 | occurs (t::ts) = occur t orelse occurs ts
63.12 @@ -160,7 +160,7 @@
63.13 Warning: finds a rigid occurrence of ?f in ?f(t).
63.14 Should NOT be called in this case: there is a flex-flex unifier
63.15 *)
63.16 -fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
63.17 +fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
63.18 let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
63.19 else NoOcc
63.20 fun occurs [] = NoOcc
63.21 @@ -230,7 +230,7 @@
63.22 If v occurs nonrigidly then must use full algorithm. *)
63.23 fun assignment thy (env, rbinder, t, u) =
63.24 let val vT as (v,T) = get_eta_var (rbinder, 0, t)
63.25 - in case rigid_occurs_term (ref [], env, v, u) of
63.26 + in case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
63.27 NoOcc => let val env = unify_types thy (body_type env T,
63.28 fastype env (rbinder,u),env)
63.29 in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
63.30 @@ -429,7 +429,7 @@
63.31 Attempts to update t with u, raising ASSIGN if impossible*)
63.32 fun ff_assign thy (env, rbinder, t, u) : Envir.env =
63.33 let val vT as (v,T) = get_eta_var(rbinder,0,t)
63.34 -in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
63.35 +in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
63.36 else let val env = unify_types thy (body_type env T,
63.37 fastype env (rbinder,u),
63.38 env)