--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/multithreading.ML Mon Sep 24 13:53:26 2007 +0200
@@ -0,0 +1,43 @@
+(* Title: Pure/ML-Systems/multithreading.ML
+ ID: $Id$
+ Author: Makarius
+
+Dummy implementation of multithreading interface.
+*)
+
+signature MULTITHREADING =
+sig
+ val trace: int ref
+ val tracing: int -> (unit -> string) -> unit
+ val available: bool
+ val max_threads: int ref
+ val self_critical: unit -> bool
+ val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
+ val CRITICAL: (unit -> 'a) -> 'a
+ datatype 'a task =
+ Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
+ val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
+end;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+val trace = ref (0: int);
+fun tracing _ _ = ();
+
+val available = false;
+val max_threads = ref (1: int);
+
+fun self_critical () = false;
+fun NAMED_CRITICAL _ e = e ();
+fun CRITICAL e = e ();
+
+datatype 'a task =
+ Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
+
+fun schedule _ _ _ = raise Fail "No multithreading support";
+
+end;
+
+val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
+val CRITICAL = Multithreading.CRITICAL;
--- a/src/Pure/ML-Systems/multithreading_dummy.ML Mon Sep 24 13:52:51 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Pure/ML-Systems/multithreading_dummy.ML
- ID: $Id$
- Author: Makarius
-
-Compatibility file for ML systems without multithreading.
-*)
-
-signature MULTITHREADING =
-sig
- val trace: int ref
- val tracing: int -> (unit -> string) -> unit
- val available: bool
- val max_threads: int ref
- val self_critical: unit -> bool
- val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
- val CRITICAL: (unit -> 'a) -> 'a
- datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
- val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
-end;
-
-structure Multithreading: MULTITHREADING =
-struct
-
-val trace = ref (0: int);
-fun tracing _ _ = ();
-
-val available = false;
-val max_threads = ref (1: int);
-
-fun self_critical () = false;
-fun NAMED_CRITICAL _ e = e ();
-fun CRITICAL e = e ();
-
-datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-
-fun schedule _ _ _ = raise Fail "No multithreading support";
-
-end;
-
-val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
-val CRITICAL = Multithreading.CRITICAL;