# HG changeset patch
# User wenzelm
# Date 1190634806 -7200
# Node ID c661dae1070ac5c113f161cb2d9aeb158ab42ac5
# Parent  ac5b5a6155ddb79f22fda6b263c1fa60076cb496
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;

diff -r ac5b5a6155dd -r c661dae1070a src/Pure/ML-Systems/multithreading.ML
--- /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;
diff -r ac5b5a6155dd -r c661dae1070a src/Pure/ML-Systems/multithreading_dummy.ML
--- 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;