--- a/src/Pure/Concurrent/event_timer.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Sat Apr 09 14:00:23 2016 +0200
@@ -109,7 +109,7 @@
manager_loop);
fun shutdown () =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
if is_shutdown Normal st then (false, st)
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
@@ -144,7 +144,7 @@
val manager' = manager_check manager;
in (canceled, make_state (requests', status, manager')) end);
-val future = Multithreading.uninterruptible (fn _ => fn time =>
+val future = Thread_Attributes.uninterruptible (fn _ => fn time =>
let
val req: request Single_Assignment.var = Single_Assignment.var "request";
fun abort () = ignore (cancel (Single_Assignment.await req));
--- a/src/Pure/Concurrent/future.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Apr 09 14:00:23 2016 +0200
@@ -206,10 +206,10 @@
broadcast scheduler_event);
fun interruptible_task f x =
- Multithreading.with_attributes
+ Thread_Attributes.with_attributes
(if is_some (worker_task ())
- then Multithreading.private_interrupts
- else Multithreading.public_interrupts)
+ then Thread_Attributes.private_interrupts
+ else Thread_Attributes.public_interrupts)
(fn _ => f x)
before Multithreading.interrupted ();
@@ -359,8 +359,8 @@
fun scheduler_loop () =
(while
- Multithreading.with_attributes
- (Multithreading.sync_interrupts Multithreading.public_interrupts)
+ Thread_Attributes.with_attributes
+ (Thread_Attributes.sync_interrupts Thread_Attributes.public_interrupts)
(fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
do (); last_round := Time.zeroTime);
@@ -438,7 +438,7 @@
val res =
if ok then
Exn.capture (fn () =>
- Multithreading.with_attributes atts (fn _ =>
+ Thread_Attributes.with_attributes atts (fn _ =>
(Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
else Exn.interrupt_exn;
in assign_result group result (identify_result pos res) end;
@@ -462,8 +462,8 @@
let
val atts =
if interrupts
- then Multithreading.private_interrupts
- else Multithreading.no_interrupts;
+ then Thread_Attributes.private_interrupts
+ else Thread_Attributes.no_interrupts;
val (result, job) = future_job grp atts e;
val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
val future = Future {promised = false, task = task, result = result};
@@ -504,7 +504,7 @@
(NONE, []) => NONE
| (NONE, deps') =>
(worker_waiting deps' (fn () =>
- Multithreading.with_attributes atts (fn _ =>
+ Thread_Attributes.with_attributes atts (fn _ =>
Exn.release (worker_wait Waiting work_finished)));
join_next atts deps')
| (SOME work, deps') => SOME (work, deps'));
@@ -521,7 +521,7 @@
val _ =
if forall is_finished xs then ()
else if is_some (worker_task ()) then
- Multithreading.with_attributes Multithreading.no_interrupts
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
(fn orig_atts => join_loop orig_atts (map task_of xs))
else List.app (ignore o Single_Assignment.await o result_of) xs;
in map get_result xs end;
@@ -544,7 +544,7 @@
(* task context for running thread *)
fun task_context name group f x =
- Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
let
val (result, job) = future_job group orig_atts (fn () => f x);
val task =
@@ -581,7 +581,7 @@
val task = task_of x;
val group = Task_Queue.group_of_task task;
val (result, job) =
- future_job group Multithreading.private_interrupts (fn () => f (join x));
+ future_job group Thread_Attributes.private_interrupts (fn () => f (join x));
val extended = SYNCHRONIZED "extend" (fn () =>
(case Task_Queue.extend task job (! queue) of
@@ -609,7 +609,7 @@
then raise Fail "Concurrent attempt to fulfill promise"
else Exn.reraise exn;
fun job () =
- Multithreading.with_attributes Multithreading.no_interrupts
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
@@ -626,7 +626,7 @@
fun job ok =
assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
val _ =
- Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
let
val passive_job =
SYNCHRONIZED "fulfill_result" (fn () =>
--- a/src/Pure/Concurrent/lazy.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML Sat Apr 09 14:00:23 2016 +0200
@@ -61,7 +61,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val (expr, x) =
Synchronized.change_result var
--- a/src/Pure/Concurrent/multithreading.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Sat Apr 09 14:00:23 2016 +0200
@@ -6,13 +6,7 @@
signature MULTITHREADING =
sig
- val no_interrupts: Thread.threadAttribute list
- val public_interrupts: Thread.threadAttribute list
- val private_interrupts: Thread.threadAttribute list
- val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
val interrupted: unit -> unit (*exception Interrupt*)
- val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
- val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
val max_threads_value: unit -> int
val max_threads_update: int -> unit
val enabled: unit -> bool
@@ -28,50 +22,16 @@
structure Multithreading: MULTITHREADING =
struct
-(* thread attributes *)
-
-val no_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val test_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
-
-val public_interrupts =
- [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val private_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val sync_interrupts = map
- (fn x as Thread.InterruptState Thread.InterruptDefer => x
- | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
- | x => x);
-
-val safe_interrupts = map
- (fn Thread.InterruptState Thread.InterruptAsynch =>
- Thread.InterruptState Thread.InterruptAsynchOnce
- | x => x);
+(* interrupts *)
fun interrupted () =
let
- val orig_atts = safe_interrupts (Thread.getAttributes ());
- val _ = Thread.setAttributes test_interrupts;
+ val orig_atts = Thread_Attributes.safe_interrupts (Thread.getAttributes ());
+ val _ = Thread.setAttributes Thread_Attributes.test_interrupts;
val test = Exn.capture Thread.testInterrupt ();
val _ = Thread.setAttributes orig_atts;
in Exn.release test end;
-fun with_attributes new_atts e =
- let
- val orig_atts = safe_interrupts (Thread.getAttributes ());
- val result = Exn.capture (fn () =>
- (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
- val _ = Thread.setAttributes orig_atts;
- in Exn.release result end;
-
-fun uninterruptible f x =
- with_attributes no_interrupts (fn atts =>
- f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
(* options *)
@@ -93,8 +53,9 @@
(* synchronous wait *)
fun sync_wait opt_atts time cond lock =
- with_attributes
- (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+ Thread_Attributes.with_attributes
+ (Thread_Attributes.sync_interrupts
+ (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
(fn _ =>
(case time of
SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
@@ -108,7 +69,7 @@
fun tracing level msg =
if level > ! trace then ()
- else uninterruptible (fn _ => fn () =>
+ else Thread_Attributes.uninterruptible (fn _ => fn () =>
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
handle _ (*sic*) => ()) ();
@@ -131,7 +92,7 @@
(* synchronized evaluation *)
fun synchronized name lock e =
- Exn.release (uninterruptible (fn restore_attributes => fn () =>
+ Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val immediate =
if Mutex.trylock lock then true
--- a/src/Pure/Concurrent/par_list.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/par_list.ML Sat Apr 09 14:00:23 2016 +0200
@@ -33,7 +33,7 @@
if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
then map (Exn.capture f) xs
else
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val (group, pri) =
(case Future.worker_task () of
--- a/src/Pure/Concurrent/single_assignment.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Sat Apr 09 14:00:23 2016 +0200
@@ -48,7 +48,7 @@
(case peek v of
SOME _ => raise Fail ("Duplicate assignment to " ^ name)
| NONE =>
- Multithreading.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible (fn _ => fn () =>
(SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
end;
--- a/src/Pure/Concurrent/standard_thread.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.ML Sat Apr 09 14:00:23 2016 +0200
@@ -50,7 +50,7 @@
fun attributes ({stack_limit, interrupts, ...}: params) =
Thread.MaximumMLStack stack_limit ::
- (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+ (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
fun fork (params: params) body =
Thread.fork (fn () =>
--- a/src/Pure/Concurrent/synchronized.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Sat Apr 09 14:00:23 2016 +0200
@@ -51,7 +51,7 @@
| Exn.Res false => NONE
| Exn.Exn exn => Exn.reraise exn)
| SOME (y, x') =>
- Multithreading.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible (fn _ => fn () =>
(var := x'; ConditionVar.broadcast cond; SOME y)) ())
end;
in try_change () end);
--- a/src/Pure/Concurrent/task_queue.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Sat Apr 09 14:00:23 2016 +0200
@@ -135,7 +135,7 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
fun update_timing update (Task {timing, ...}) e =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val start = Time.now ();
val result = Exn.capture (restore_attributes e) ();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_attributes.ML Sat Apr 09 14:00:23 2016 +0200
@@ -0,0 +1,63 @@
+(* Title: Pure/Concurrent/thread_attributes.ML
+ Author: Makarius
+
+Thread attributes for interrupt handling.
+*)
+
+signature THREAD_ATTRIBUTES =
+sig
+ type attributes = Thread.Thread.threadAttribute list
+ val no_interrupts: attributes
+ val test_interrupts: attributes
+ val public_interrupts: attributes
+ val private_interrupts: attributes
+ val sync_interrupts: attributes -> attributes
+ val safe_interrupts: attributes -> attributes
+ val with_attributes: attributes -> (attributes -> 'a) -> 'a
+ val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+end;
+
+structure Thread_Attributes: THREAD_ATTRIBUTES =
+struct
+
+type attributes = Thread.Thread.threadAttribute list;
+
+val no_interrupts =
+ [Thread.Thread.EnableBroadcastInterrupt false,
+ Thread.Thread.InterruptState Thread.Thread.InterruptDefer];
+
+val test_interrupts =
+ [Thread.Thread.EnableBroadcastInterrupt false,
+ Thread.Thread.InterruptState Thread.Thread.InterruptSynch];
+
+val public_interrupts =
+ [Thread.Thread.EnableBroadcastInterrupt true,
+ Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+
+val private_interrupts =
+ [Thread.Thread.EnableBroadcastInterrupt false,
+ Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+
+val sync_interrupts = map
+ (fn x as Thread.Thread.InterruptState Thread.Thread.InterruptDefer => x
+ | Thread.Thread.InterruptState _ => Thread.Thread.InterruptState Thread.Thread.InterruptSynch
+ | x => x);
+
+val safe_interrupts = map
+ (fn Thread.Thread.InterruptState Thread.Thread.InterruptAsynch =>
+ Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce
+ | x => x);
+
+fun with_attributes new_atts e =
+ let
+ val orig_atts = safe_interrupts (Thread.Thread.getAttributes ());
+ val result = Exn.capture (fn () =>
+ (Thread.Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
+ val _ = Thread.Thread.setAttributes orig_atts;
+ in Exn.release result end;
+
+fun uninterruptible f x =
+ with_attributes no_interrupts (fn atts =>
+ f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+
+end;
--- a/src/Pure/Concurrent/thread_data.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/thread_data.ML Sat Apr 09 14:00:23 2016 +0200
@@ -17,70 +17,20 @@
structure Thread_Data: THREAD_DATA =
struct
-open Thread;
-
-
-(* exceptions as values *)
-
-structure Exn =
-struct
-
-datatype 'a result =
- Res of 'a |
- Exn of exn;
-
-fun capture f x = Res (f x) handle e => Exn e;
-
-fun release (Res y) = y
- | release (Exn e) = PolyML.Exception.reraise e;
-
-end;
-
-
-(* thread attributes *)
-
-structure Multithreading =
-struct
-
-val no_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val safe_interrupts = map
- (fn Thread.InterruptState Thread.InterruptAsynch =>
- Thread.InterruptState Thread.InterruptAsynchOnce
- | x => x);
-
-fun with_attributes new_atts e =
- let
- val orig_atts = safe_interrupts (Thread.getAttributes ());
- val result = Exn.capture (fn () =>
- (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
- val _ = Thread.setAttributes orig_atts;
- in Exn.release result end;
-
-fun uninterruptible f x =
- with_attributes no_interrupts (fn atts =>
- f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
-end;
-
-
-(* var *)
-
abstype 'a var = Var of 'a option Universal.tag
with
fun var () : 'a var = Var (Universal.tag ());
fun get (Var tag) =
- (case Thread.getLocal tag of
+ (case Thread.Thread.getLocal tag of
SOME data => data
| NONE => NONE);
-fun put (Var tag) data = Thread.setLocal (tag, data);
+fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
fun setmp v data f x =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val orig_data = get v;
val _ = put v data;
--- a/src/Pure/Concurrent/thread_data_virtual.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML Sat Apr 09 14:00:23 2016 +0200
@@ -7,8 +7,6 @@
structure Thread_Data_Virtual: THREAD_DATA =
struct
-(* context data *)
-
structure Data = Generic_Data
(
type T = Universal.universal Inttab.table;
@@ -33,7 +31,7 @@
| SOME x => Inttab.update (i, Universal.tagInject tag x));
fun setmp v data f x =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val orig_data = get v;
val _ = put v data;
--- a/src/Pure/Concurrent/timeout.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML Sat Apr 09 14:00:23 2016 +0200
@@ -17,7 +17,7 @@
exception TIMEOUT of Time.time;
fun apply timeout f x =
- Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
let
val self = Thread.self ();
val start = Time.now ();
@@ -26,7 +26,7 @@
Event_Timer.request (start + timeout)
(fn () => Standard_Thread.interrupt_unsynchronized self);
val result =
- Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+ Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
val stop = Time.now ();
val was_timeout = not (Event_Timer.cancel request);
--- a/src/Pure/Concurrent/unsynchronized.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Sat Apr 09 14:00:23 2016 +0200
@@ -19,7 +19,7 @@
fun dec i = (i := ! i - (1: int); ! i);
fun setmp flag value f x =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val orig_value = ! flag;
val _ = flag := value;
--- a/src/Pure/General/exn.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/General/exn.ML Sat Apr 09 14:00:23 2016 +0200
@@ -127,8 +127,3 @@
in reraise exn end);
end;
-
-datatype illegal = Interrupt;
-
-structure Basic_Exn: BASIC_EXN = Exn;
-open Basic_Exn;
--- a/src/Pure/ML/exn_debugger.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML Sat Apr 09 14:00:23 2016 +0200
@@ -42,7 +42,7 @@
in
fun capture_exception_trace e =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val _ = start_trace ();
val result = Exn.interruptible_capture (restore_attributes e) ();
--- a/src/Pure/ML/exn_properties.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/exn_properties.ML Sat Apr 09 14:00:23 2016 +0200
@@ -63,7 +63,7 @@
startLine = #startLine loc, endLine = #endLine loc,
startPosition = #startPosition loc, endPosition = #endPosition loc};
in
- Multithreading.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible (fn _ => fn () =>
PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
end
end;
--- a/src/Pure/ML/ml_name_space.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Sat Apr 09 14:00:23 2016 +0200
@@ -63,11 +63,11 @@
val bootstrap_values =
["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
"chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
+ val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
val bootstrap_structures =
- ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data",
- "ML_Recursive"];
+ ["Exn", "Basic_Exn", "Thread_Data", "ML_Recursive", "PolyML"] @ hidden_structures;
val bootstrap_signatures =
- ["THREAD_DATA", "ML_RECURSIVE"];
+ ["EXN", "BASIC_EXN", "THREAD_DATA", "ML_RECURSIVE"];
(* Standard ML environment *)
--- a/src/Pure/ML/ml_pervasive0.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_pervasive0.ML Sat Apr 09 14:00:23 2016 +0200
@@ -26,3 +26,8 @@
val error_depth = PolyML.error_depth;
open Thread;
+
+datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
--- a/src/Pure/ML/ml_pervasive1.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML Sat Apr 09 14:00:23 2016 +0200
@@ -4,8 +4,7 @@
Pervasive ML environment: final setup.
*)
-List.app ML_Name_Space.forget_structure
- (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
structure PolyML = struct structure IntInf = PolyML.IntInf end;
--- a/src/Pure/PIDE/execution.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/PIDE/execution.ML Sat Apr 09 14:00:23 2016 +0200
@@ -89,7 +89,7 @@
type params = {name: string, pos: Position.T, pri: int};
fun fork ({name, pos, pri}: params) e =
- Multithreading.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
+ Thread_Attributes.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
let
val exec_id = the_default 0 (Position.parse_id pos);
val group = Future.worker_subgroup ();
--- a/src/Pure/PIDE/query_operation.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/PIDE/query_operation.ML Sat Apr 09 14:00:23 2016 +0200
@@ -19,7 +19,7 @@
Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
- print_fn = fn _ => Multithreading.uninterruptible (fn restore_attributes => fn state =>
+ print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
let
fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = output_result (Markup.markup_only m);
--- a/src/Pure/ROOT.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ROOT.ML Sat Apr 09 14:00:23 2016 +0200
@@ -9,7 +9,6 @@
ML_file "ML/ml_system.ML";
ML_file "System/distribution.ML";
-ML_file "General/exn.ML";
ML_file "General/basics.ML";
ML_file "Concurrent/multithreading.ML";
--- a/src/Pure/ROOT0.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ROOT0.ML Sat Apr 09 14:00:23 2016 +0200
@@ -1,4 +1,8 @@
(*** Isabelle/Pure bootstrap: initial setup ***)
+ML_file "General/exn.ML";
+
+ML_file "Concurrent/thread_attributes.ML";
ML_file "Concurrent/thread_data.ML";
-ML_file "ML/ml_recursive.ML"
+
+ML_file "ML/ml_recursive.ML";
--- a/src/Pure/System/bash.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/bash.ML Sat Apr 09 14:00:23 2016 +0200
@@ -14,7 +14,7 @@
structure Bash: BASH =
struct
-val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
+val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
@@ -34,7 +34,7 @@
val system_thread =
Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
val bash_script =
@@ -105,7 +105,7 @@
structure Bash: BASH =
struct
-val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
+val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
@@ -125,7 +125,7 @@
val system_thread =
Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
val _ = getenv_strict "ISABELLE_BASH_PROCESS";
--- a/src/Pure/System/command_line.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/command_line.ML Sat Apr 09 14:00:23 2016 +0200
@@ -14,7 +14,7 @@
struct
fun tool body =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val rc =
restore_attributes body () handle exn =>
--- a/src/Pure/System/isabelle_process.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML Sat Apr 09 14:00:23 2016 +0200
@@ -187,7 +187,7 @@
val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
-val init_protocol = Multithreading.uninterruptible (fn _ => fn socket =>
+val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
let
val _ = SHA1.test_samples ()
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
--- a/src/Pure/Thy/thy_info.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Apr 09 14:00:23 2016 +0200
@@ -185,7 +185,7 @@
in result_theory result end
| Finished thy => thy)) #> ignore;
-val schedule_futures = Multithreading.uninterruptible (fn _ => fn tasks =>
+val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
let
val futures = tasks
|> String_Graph.schedule (fn deps => fn (name, task) =>
--- a/src/Pure/Tools/debugger.ML Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Tools/debugger.ML Sat Apr 09 14:00:23 2016 +0200
@@ -227,7 +227,7 @@
in
fun debugger_loop thread_name =
- Multithreading.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
fun loop () =
(debugger_state thread_name; if debugger_command thread_name then loop () else ());