Compatibility file for ML systems without multithreading.
authorwenzelm
Tue, 24 Jul 2007 19:44:31 +0200
changeset 23960 c07ae96cbfc4
parent 23959 c2e81bcee06b
child 23961 9e7e1e309ebd
Compatibility file for ML systems without multithreading.
src/Pure/ML-Systems/multithreading_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Tue Jul 24 19:44:31 2007 +0200
@@ -0,0 +1,25 @@
+(*  Title:      Pure/ML-Systems/multithreading_dummy.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Compatibility file for ML systems without multithreading.
+*)
+
+signature MULTITHREADING =
+sig
+  val number_of_threads: int ref
+  val self_critical: unit -> bool
+  val CRITICAL: (unit -> 'a) -> 'a
+end;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+val number_of_threads = ref 0;
+
+fun self_critical () = false;
+fun CRITICAL e = e ();
+
+end;
+
+val CRITICAL = Multithreading.CRITICAL;