--- a/lib/scripts/process Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# exec process - with optional process group and report of pid
-#
-
-use warnings;
-use strict;
-
-# process group
-
-my $group = $ARGV[0]; shift(@ARGV);
-
-if ($group eq "group") {
- use POSIX "setsid";
- POSIX::setsid || die $!;
-}
-
-
-# report pid
-
-my $pid_name = $ARGV[0]; shift(@ARGV);
-
-if ($pid_name eq "-") {
- print "$$\n";
-}
-else {
- open (PID_FILE, ">", $pid_name) || die $!;
- print PID_FILE "$$";
- close PID_FILE;
-}
-
-
-# exec process
-
-my $script = $ARGV[0]; shift(@ARGV);
-
-if ($script eq "script") {
- my $cmd_line = $ARGV[0]; shift(@ARGV);
- exec $cmd_line || die $!;
-}
-else {
- (exec { $ARGV[0] } @ARGV) || die $!;
-}
-
--- a/src/Pure/Concurrent/bash_sequential.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: Pure/Concurrent/bash_sequential.ML
- Author: Makarius
-
-Generic GNU bash processes (no provisions to propagate interrupts, but
-could work via the controlling tty).
-*)
-
-signature BASH =
-sig
- val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-fun process script =
- let
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
- in
- let
- val _ = File.write script_path script;
- val status =
- OS.Process.system
- ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
- " script \"exec bash " ^ File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path ^ "\"");
- val rc =
- (case Posix.Process.fromStatus status of
- Posix.Process.W_EXITED => 0
- | Posix.Process.W_EXITSTATUS w => Word8.toInt w
- | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
- | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
- val out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => ()} end
- handle exn => (cleanup (); reraise exn)
- end;
-
-end;
-
--- a/src/Pure/Concurrent/future.ML Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Feb 18 23:10:28 2016 +0100
@@ -199,13 +199,11 @@
broadcast scheduler_event);
fun interruptible_task f x =
- (if Multithreading.available then
- Multithreading.with_attributes
- (if is_some (worker_task ())
- then Multithreading.private_interrupts
- else Multithreading.public_interrupts)
- (fn _ => f x)
- else interruptible f x)
+ Multithreading.with_attributes
+ (if is_some (worker_task ())
+ then Multithreading.private_interrupts
+ else Multithreading.public_interrupts)
+ (fn _ => f x)
before Multithreading.interrupted ();
@@ -651,8 +649,7 @@
(* shutdown *)
fun shutdown () =
- if not Multithreading.available then ()
- else if is_some (worker_task ()) then
+ if is_some (worker_task ()) then
raise Fail "Cannot shutdown while running as worker thread"
else
SYNCHRONIZED "shutdown" (fn () =>
--- a/src/Pure/Concurrent/lazy_sequential.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: Pure/Concurrent/lazy_sequential.ML
- Author: Florian Haftmann and Makarius, TU Muenchen
-
-Lazy evaluation with memoing of results and regular exceptions
-(sequential version).
-*)
-
-structure Lazy: LAZY =
-struct
-
-(* datatype *)
-
-datatype 'a expr =
- Expr of unit -> 'a |
- Result of 'a Exn.result;
-
-abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
-with
-
-fun lazy e = Lazy (Unsynchronized.ref (Expr e));
-fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
-
-fun peek (Lazy r) =
- (case ! r of
- Expr _ => NONE
- | Result res => SOME res);
-
-fun is_running _ = false;
-fun is_finished x = is_some (peek x);
-val finished_result = peek;
-
-
-(* force result *)
-
-fun force_result (Lazy r) =
- let
- val result =
- (case ! r of
- Expr e => Exn.capture e ()
- | Result res => res);
- val _ = if Exn.is_interrupt_exn result then () else r := Result result;
- in result end;
-
-fun force r = Exn.release (force_result r);
-fun map f x = lazy (fn () => f (force x));
-
-
-(* future evaluation *)
-
-fun future params x =
- if is_finished x then Future.value_result (force_result x)
- else (singleton o Future.forks) params (fn () => force x);
-
-end;
-end;
-
-type 'a lazy = 'a Lazy.lazy;
-
--- a/src/Pure/Concurrent/par_list_sequential.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/Concurrent/par_list_sequential.ML
- Author: Makarius
-
-Dummy version of parallel list combinators -- plain sequential evaluation.
-*)
-
-structure Par_List: PAR_LIST =
-struct
-
-fun managed_results _ f = map (Exn.capture f);
-fun map_name _ = map;
-val map = map;
-val map_independent = map;
-val get_some = get_first;
-val find_some = find_first;
-val exists = exists;
-val forall = forall;
-
-end;
--- a/src/Pure/Concurrent/single_assignment_sequential.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: Pure/Concurrent/single_assignment_sequential.ML
- Author: Makarius
-
-Single-assignment variables (sequential version).
-*)
-
-structure Single_Assignment: SINGLE_ASSIGNMENT =
-struct
-
-abstype 'a var = Var of 'a SingleAssignment.saref
-with
-
-fun var _ = Var (SingleAssignment.saref ());
-
-fun peek (Var var) = SingleAssignment.savalue var;
-
-fun await v =
- (case peek v of
- SOME x => x
- | NONE => Thread.unavailable ());
-
-fun assign (v as Var var) x =
- (case peek v of
- SOME _ => raise Fail "Duplicate assignment to variable"
- | NONE => SingleAssignment.saset (var, x));
-
-end;
-
-end;
-
--- a/src/Pure/Concurrent/synchronized_sequential.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: Pure/Concurrent/synchronized_sequential.ML
- Author: Makarius
-
-Sequential version of state variables -- plain refs.
-*)
-
-structure Synchronized: SYNCHRONIZED =
-struct
-
-abstype 'a var = Var of 'a Unsynchronized.ref
-with
-
-fun var _ x = Var (Unsynchronized.ref x);
-fun value (Var var) = ! var;
-
-fun timed_access (Var var) _ f =
- (case f (! var) of
- SOME (y, x') => (var := x'; SOME y)
- | NONE => Thread.unavailable ());
-
-fun guarded_access var f = the (timed_access var (K NONE) f);
-
-fun change_result var f = guarded_access var (SOME o f);
-fun change var f = change_result var (fn x => ((), f x));
-
-end;
-
-end;
--- a/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Thu Feb 18 23:10:28 2016 +0100
@@ -75,7 +75,6 @@
open Thread;
use "RAW/multithreading.ML";
-use "RAW/multithreading_polyml.ML";
if ML_System.name = "polyml-5.6"
then use "RAW/ml_stack_polyml-5.6.ML"
--- a/src/Pure/RAW/multithreading.ML Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/RAW/multithreading.ML Thu Feb 18 23:10:28 2016 +0100
@@ -1,22 +1,28 @@
(* Title: Pure/RAW/multithreading.ML
Author: Makarius
-Dummy implementation of multithreading setup.
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
*)
+signature BASIC_MULTITHREADING =
+sig
+ val interruptible: ('a -> 'b) -> 'a -> 'b
+ val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+end;
+
signature MULTITHREADING =
sig
- val available: bool
- val max_threads_value: unit -> int
- val max_threads_update: int -> unit
- val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
- val enabled: unit -> bool
+ include BASIC_MULTITHREADING
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 max_threads_value: unit -> int
+ val max_threads_update: int -> unit
+ val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
+ val enabled: unit -> bool
val sync_wait: Thread.threadAttribute list option -> Time.time option ->
ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
val trace: int ref
@@ -30,46 +36,156 @@
structure Multithreading: MULTITHREADING =
struct
-(* options *)
+(* 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 available = false;
-fun max_threads_value () = 1: int;
-fun max_threads_update _ = ();
-fun max_threads_setmp _ f x = f x;
-fun enabled () = false;
+val safe_interrupts = map
+ (fn Thread.InterruptState Thread.InterruptAsynch =>
+ Thread.InterruptState Thread.InterruptAsynchOnce
+ | x => x);
+
+fun interrupted () =
+ let
+ val orig_atts = safe_interrupts (Thread.getAttributes ());
+ val _ = Thread.setAttributes 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;
-(* attributes *)
+(* portable wrappers *)
+
+fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
+
+fun uninterruptible f x =
+ with_attributes no_interrupts (fn atts =>
+ f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+
+
+(* options *)
+
+fun max_threads_result m =
+ if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
+
+val max_threads = ref 1;
+
+fun max_threads_value () = ! max_threads;
+
+fun max_threads_update m = max_threads := max_threads_result m;
-val no_interrupts = [];
-val public_interrupts = [];
-val private_interrupts = [];
-fun sync_interrupts _ = [];
+fun max_threads_setmp m f x =
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val max_threads_orig = ! max_threads;
+ val _ = max_threads_update m;
+ val result = Exn.capture (restore_attributes f) x;
+ val _ = max_threads := max_threads_orig;
+ in Exn.release result end) ();
+
+fun enabled () = max_threads_value () > 1;
-fun interrupted () = ();
+
+(* synchronous wait *)
-fun with_attributes _ e = e [];
-
-fun sync_wait _ _ _ _ = Exn.Res true;
+fun sync_wait opt_atts time cond lock =
+ with_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))
+ | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
+ handle exn => Exn.Exn exn);
(* tracing *)
-val trace = ref (0: int);
-fun tracing _ _ = ();
-fun tracing_time _ _ _ = ();
-fun real_time f x = (f x; Time.zeroTime);
+val trace = ref 0;
+
+fun tracing level msg =
+ if level > ! trace then ()
+ else uninterruptible (fn _ => fn () =>
+ (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+ handle _ (*sic*) => ()) ();
+
+fun tracing_time detailed time =
+ tracing
+ (if not detailed then 5
+ else if Time.>= (time, seconds 1.0) then 1
+ else if Time.>= (time, seconds 0.1) then 2
+ else if Time.>= (time, seconds 0.01) then 3
+ else if Time.>= (time, seconds 0.001) then 4 else 5);
+
+fun real_time f x =
+ let
+ val timer = Timer.startRealTimer ();
+ val () = f x;
+ val time = Timer.checkRealTimer timer;
+ in time end;
(* synchronized evaluation *)
-fun synchronized _ _ e = e ();
+fun synchronized name lock e =
+ Exn.release (uninterruptible (fn restore_attributes => fn () =>
+ let
+ val immediate =
+ if Mutex.trylock lock then true
+ else
+ let
+ val _ = tracing 5 (fn () => name ^ ": locking ...");
+ val time = real_time Mutex.lock lock;
+ val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+ in false end;
+ val result = Exn.capture (restore_attributes e) ();
+ val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+ val _ = Mutex.unlock lock;
+ in result end) ());
(* serial numbers *)
-local val count = ref (0: int)
-in fun serial () = (count := ! count + 1; ! count) end;
+local
+
+val serial_lock = Mutex.mutex ();
+val serial_count = ref 0;
+
+in
+
+val serial = uninterruptible (fn _ => fn () =>
+ let
+ val _ = Mutex.lock serial_lock;
+ val _ = serial_count := ! serial_count + 1;
+ val res = ! serial_count;
+ val _ = Mutex.unlock serial_lock;
+ in res end);
end;
+end;
+
+structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
+open Basic_Multithreading;
--- a/src/Pure/RAW/multithreading_polyml.ML Wed Feb 17 23:29:35 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* Title: Pure/RAW/multithreading_polyml.ML
- Author: Makarius
-
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
-*)
-
-signature MULTITHREADING =
-sig
- include MULTITHREADING
- val interruptible: ('a -> 'b) -> 'a -> 'b
- val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
-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);
-
-fun interrupted () =
- let
- val orig_atts = safe_interrupts (Thread.getAttributes ());
- val _ = Thread.setAttributes 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;
-
-
-(* portable wrappers *)
-
-fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
-
-fun uninterruptible f x =
- with_attributes no_interrupts (fn atts =>
- f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
-
-(* options *)
-
-val available = true;
-
-fun max_threads_result m =
- if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
-
-val max_threads = ref 1;
-
-fun max_threads_value () = ! max_threads;
-
-fun max_threads_update m = max_threads := max_threads_result m;
-
-fun max_threads_setmp m f x =
- uninterruptible (fn restore_attributes => fn () =>
- let
- val max_threads_orig = ! max_threads;
- val _ = max_threads_update m;
- val result = Exn.capture (restore_attributes f) x;
- val _ = max_threads := max_threads_orig;
- in Exn.release result end) ();
-
-fun enabled () = max_threads_value () > 1;
-
-
-(* synchronous wait *)
-
-fun sync_wait opt_atts time cond lock =
- with_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))
- | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
- handle exn => Exn.Exn exn);
-
-
-(* tracing *)
-
-val trace = ref 0;
-
-fun tracing level msg =
- if level > ! trace then ()
- else uninterruptible (fn _ => fn () =>
- (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
- handle _ (*sic*) => ()) ();
-
-fun tracing_time detailed time =
- tracing
- (if not detailed then 5
- else if Time.>= (time, seconds 1.0) then 1
- else if Time.>= (time, seconds 0.1) then 2
- else if Time.>= (time, seconds 0.01) then 3
- else if Time.>= (time, seconds 0.001) then 4 else 5);
-
-fun real_time f x =
- let
- val timer = Timer.startRealTimer ();
- val () = f x;
- val time = Timer.checkRealTimer timer;
- in time end;
-
-
-(* synchronized evaluation *)
-
-fun synchronized name lock e =
- Exn.release (uninterruptible (fn restore_attributes => fn () =>
- let
- val immediate =
- if Mutex.trylock lock then true
- else
- let
- val _ = tracing 5 (fn () => name ^ ": locking ...");
- val time = real_time Mutex.lock lock;
- val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
- in false end;
- val result = Exn.capture (restore_attributes e) ();
- val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
- val _ = Mutex.unlock lock;
- in result end) ());
-
-
-(* serial numbers *)
-
-local
-
-val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
-
-in
-
-val serial = uninterruptible (fn _ => fn () =>
- let
- val _ = Mutex.lock serial_lock;
- val _ = serial_count := ! serial_count + 1;
- val res = ! serial_count;
- val _ = Mutex.unlock serial_lock;
- in res end);
-
-end;
-
-end;
-
-val interruptible = Multithreading.interruptible;
-val uninterruptible = Multithreading.uninterruptible;
-
--- a/src/Pure/ROOT Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/ROOT Thu Feb 18 23:10:28 2016 +0100
@@ -25,7 +25,6 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/multithreading_polyml.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -57,7 +56,6 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/multithreading_polyml.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -65,24 +63,19 @@
"RAW/windows_path.ML"
"Concurrent/bash.ML"
- "Concurrent/bash_sequential.ML"
"Concurrent/bash_windows.ML"
"Concurrent/cache.ML"
"Concurrent/counter.ML"
"Concurrent/event_timer.ML"
"Concurrent/future.ML"
"Concurrent/lazy.ML"
- "Concurrent/lazy_sequential.ML"
"Concurrent/mailbox.ML"
"Concurrent/par_exn.ML"
"Concurrent/par_list.ML"
- "Concurrent/par_list_sequential.ML"
"Concurrent/random.ML"
"Concurrent/single_assignment.ML"
- "Concurrent/single_assignment_sequential.ML"
"Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
- "Concurrent/synchronized_sequential.ML"
"Concurrent/task_queue.ML"
"Concurrent/time_limit.ML"
"General/alist.ML"
--- a/src/Pure/ROOT.ML Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/ROOT.ML Thu Feb 18 23:10:28 2016 +0100
@@ -19,8 +19,6 @@
use "General/table.ML";
use "Concurrent/synchronized.ML";
-if Multithreading.available then ()
-else use "Concurrent/synchronized_sequential.ML";
use "Concurrent/counter.ML";
use "Concurrent/random.ML";
@@ -106,13 +104,10 @@
else use "ML/ml_statistics_dummy.ML";
use "Concurrent/standard_thread.ML";
+use "Concurrent/single_assignment.ML";
-use "Concurrent/single_assignment.ML";
-if Multithreading.available then ()
-else use "Concurrent/single_assignment_sequential.ML";
-
-if not Multithreading.available then use "Concurrent/bash_sequential.ML"
-else if ML_System.platform_is_windows then use "Concurrent/bash_windows.ML"
+if ML_System.platform_is_windows
+then use "Concurrent/bash_windows.ML"
else use "Concurrent/bash.ML";
use "Concurrent/par_exn.ML";
@@ -120,14 +115,8 @@
use "Concurrent/future.ML";
use "Concurrent/event_timer.ML";
use "Concurrent/time_limit.ML";
-
use "Concurrent/lazy.ML";
-if Multithreading.available then ()
-else use "Concurrent/lazy_sequential.ML";
-
use "Concurrent/par_list.ML";
-if Multithreading.available then ()
-else use "Concurrent/par_list_sequential.ML";
use "Concurrent/mailbox.ML";
use "Concurrent/cache.ML";
--- a/src/Pure/System/message_channel.ML Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/System/message_channel.ML Thu Feb 18 23:10:28 2016 +0100
@@ -56,20 +56,14 @@
in fn () => continue NONE end;
fun make channel =
- if Multithreading.available then
- let
- val mbox = Mailbox.create ();
- val thread =
- Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
- (message_output mbox channel);
- fun send msg = Mailbox.send mbox (SOME msg);
- fun shutdown () =
- (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
- in Message_Channel {send = send, shutdown = shutdown} end
- else
- let
- fun send msg = (output_message channel msg; flush channel);
- in Message_Channel {send = send, shutdown = fn () => ()} end;
+ let
+ val mbox = Mailbox.create ();
+ val thread =
+ Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+ (message_output mbox channel);
+ fun send msg = Mailbox.send mbox (SOME msg);
+ fun shutdown () =
+ (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
+ in Message_Channel {send = send, shutdown = shutdown} end;
end;
-