src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title:      Pure/ML-Systems/multithreading.ML
-    Author:     Makarius
-
-Dummy implementation of multithreading setup.
-*)
-
-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
-  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 sync_wait: Thread.threadAttribute list option -> Time.time option ->
-    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
-  val trace: int ref
-  val tracing: int -> (unit -> string) -> unit
-  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
-  val real_time: ('a -> unit) -> 'a -> Time.time
-  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
-  val serial: unit -> int
-end;
-
-structure Multithreading: MULTITHREADING =
-struct
-
-(* options *)
-
-val available = false;
-fun max_threads_value () = 1: int;
-fun max_threads_update _ = ();
-fun max_threads_setmp _ f x = f x;
-fun enabled () = false;
-
-
-(* attributes *)
-
-val no_interrupts = [];
-val public_interrupts = [];
-val private_interrupts = [];
-fun sync_interrupts _ = [];
-
-fun interrupted () = ();
-
-fun with_attributes _ e = e [];
-
-fun sync_wait _ _ _ _ = Exn.Res true;
-
-
-(* tracing *)
-
-val trace = ref (0: int);
-fun tracing _ _ = ();
-fun tracing_time _ _ _ = ();
-fun real_time f x = (f x; Time.zeroTime);
-
-
-(* synchronized evaluation *)
-
-fun synchronized _ _ e = e ();
-
-
-(* serial numbers *)
-
-local val count = ref (0: int)
-in fun serial () = (count := ! count + 1; ! count) end;
-
-end;
-