--- a/src/Pure/Concurrent/par_list_dummy.ML Thu Oct 01 18:10:41 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/Concurrent/par_list_dummy.ML
- Author: Makarius
-
-Dummy version of parallel list combinators -- plain sequential evaluation.
-*)
-
-structure Par_List: PAR_LIST =
-struct
-
-val map = map;
-val get_some = get_first;
-val find_some = find_first;
-val exists = exists;
-val forall = forall;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list_sequential.ML Thu Oct 01 18:21:11 2009 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/Concurrent/par_list_sequential.ML
+ Author: Makarius
+
+Dummy version of parallel list combinators -- plain sequential evaluation.
+*)
+
+structure Par_List: PAR_LIST =
+struct
+
+val map = map;
+val get_some = get_first;
+val find_some = find_first;
+val exists = exists;
+val forall = forall;
+
+end;
--- a/src/Pure/Concurrent/synchronized_dummy.ML Thu Oct 01 18:10:41 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: Pure/Concurrent/synchronized_dummy.ML
- Author: Makarius
-
-Dummy version of state variables -- plain refs for sequential access.
-*)
-
-structure Synchronized: SYNCHRONIZED =
-struct
-
-datatype 'a var = Var of 'a Unsynchronized.ref;
-
-fun var _ x = Var (Unsynchronized.ref x);
-fun value (Var var) = ! var;
-
-fun timed_access (Var var) _ f =
- (case f (! var) of
- SOME (y, x') => (var := x'; SOME y)
- | NONE => Thread.unavailable ());
-
-fun guarded_access var f = the (timed_access var (K NONE) f);
-
-fun change_result var f = guarded_access var (SOME o f);
-fun change var f = change_result var (fn x => ((), f x));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Thu Oct 01 18:21:11 2009 +0200
@@ -0,0 +1,27 @@
+(* Title: Pure/Concurrent/synchronized_sequential.ML
+ Author: Makarius
+
+Sequential version of state variables -- plain refs.
+*)
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+abstype 'a var = Var of 'a Unsynchronized.ref
+with
+
+fun var _ x = Var (Unsynchronized.ref x);
+fun value (Var var) = ! var;
+
+fun timed_access (Var var) _ f =
+ (case f (! var) of
+ SOME (y, x') => (var := x'; SOME y)
+ | NONE => Thread.unavailable ());
+
+fun guarded_access var f = the (timed_access var (K NONE) f);
+
+fun change_result var f = guarded_access var (SOME o f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;
+end;
--- a/src/Pure/IsaMakefile Thu Oct 01 18:10:41 2009 +0200
+++ b/src/Pure/IsaMakefile Thu Oct 01 18:21:11 2009 +0200
@@ -45,8 +45,8 @@
$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML \
Concurrent/lazy.ML Concurrent/lazy_sequential.ML \
Concurrent/mailbox.ML Concurrent/par_list.ML \
- Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
- Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML \
+ Concurrent/par_list_sequential.ML Concurrent/simple_thread.ML \
+ Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \
Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \
General/balanced_tree.ML General/basics.ML General/binding.ML \
General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
--- a/src/Pure/ROOT.ML Thu Oct 01 18:10:41 2009 +0200
+++ b/src/Pure/ROOT.ML Thu Oct 01 18:21:11 2009 +0200
@@ -57,8 +57,8 @@
use "Concurrent/simple_thread.ML";
use "Concurrent/synchronized.ML";
-if Multithreading.available then () else
-use "Concurrent/synchronized_dummy.ML";
+if Multithreading.available then ()
+else use "Concurrent/synchronized_sequential.ML";
use "Concurrent/mailbox.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
@@ -67,7 +67,7 @@
else use "Concurrent/lazy_sequential.ML";
use "Concurrent/par_list.ML";
if Multithreading.available then ()
-else use "Concurrent/par_list_dummy.ML";
+else use "Concurrent/par_list_sequential.ML";
(* fundamental structures *)