# HG changeset patch
# User wenzelm
# Date 1455834606 -3600
# Node ID 3fd79fcdb491c8e709d954ad18fae7544975bb0f
# Parent  0b7337826593f8e5a1ffeab93718481d07f803a9# Parent  6709e51d5c119bd3941a8327c07f93cc737b1c48
merged

diff -r 0b7337826593 -r 3fd79fcdb491 lib/scripts/process
--- a/lib/scripts/process	Thu Feb 18 17:07:10 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 $!;
-}
-
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/bash_sequential.ML
--- a/src/Pure/Concurrent/bash_sequential.ML	Thu Feb 18 17:07:10 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;
-
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Feb 18 23:30:06 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 () =>
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Thu Feb 18 17:07:10 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;
-
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/par_list_sequential.ML
--- a/src/Pure/Concurrent/par_list_sequential.ML	Thu Feb 18 17:07:10 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;
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/single_assignment_sequential.ML
--- a/src/Pure/Concurrent/single_assignment_sequential.ML	Thu Feb 18 17:07:10 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;
-
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Thu Feb 18 17:07:10 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;
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Feb 18 23:30:06 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"
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/RAW/multithreading.ML
--- a/src/Pure/RAW/multithreading.ML	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/RAW/multithreading.ML	Thu Feb 18 23:30:06 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;
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/RAW/multithreading_polyml.ML
--- a/src/Pure/RAW/multithreading_polyml.ML	Thu Feb 18 17:07:10 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;
-
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/ROOT	Thu Feb 18 23:30:06 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"
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Feb 18 23:30:06 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";
diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Thu Feb 18 17:07:10 2016 +0100
+++ b/src/Pure/System/message_channel.ML	Thu Feb 18 23:30:06 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;
-