author  wenzelm 
Mon, 24 Sep 2007 13:53:26 +0200  
changeset 24690  c661dae1070a 
child 25704  df9c8074ff09 
permissions  rwrr 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/multithreading.ML 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

4 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

5 
Dummy implementation of multithreading interface. 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

6 
*) 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

7 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

8 
signature MULTITHREADING = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

9 
sig 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

10 
val trace: int ref 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

11 
val tracing: int > (unit > string) > unit 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

12 
val available: bool 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

13 
val max_threads: int ref 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

14 
val self_critical: unit > bool 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

15 
val NAMED_CRITICAL: string > (unit > 'a) > 'a 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

16 
val CRITICAL: (unit > 'a) > 'a 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

17 
datatype 'a task = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

18 
Task of {body: unit > unit, cont: 'a > 'a, fail: 'a > 'a}  Wait  Terminate; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

19 
val schedule: int > ('a > 'a task * 'a) > 'a > exn list 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

20 
end; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

21 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

22 
structure Multithreading: MULTITHREADING = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

23 
struct 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

24 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

25 
val trace = ref (0: int); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

26 
fun tracing _ _ = (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

27 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

28 
val available = false; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

29 
val max_threads = ref (1: int); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

30 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

31 
fun self_critical () = false; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

32 
fun NAMED_CRITICAL _ e = e (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

33 
fun CRITICAL e = e (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

34 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

35 
datatype 'a task = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

36 
Task of {body: unit > unit, cont: 'a > 'a, fail: 'a > 'a}  Wait  Terminate; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

37 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

38 
fun schedule _ _ _ = raise Fail "No multithreading support"; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

39 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

40 
end; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

41 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

42 
val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

43 
val CRITICAL = Multithreading.CRITICAL; 