# HG changeset patch
# User wenzelm
# Date 1254414071 -7200
# Node ID 5db89f8d44f3875c48399b74f09347bbeb0b60db
# Parent  1a5e364584ae5525db115aa763b1e72b2d06df11
more official status of sequential implementations;
tuned;

diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/Concurrent/par_list_dummy.ML
--- 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;
diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/Concurrent/par_list_sequential.ML
--- /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;
diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/Concurrent/synchronized_dummy.ML
--- 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;
diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/Concurrent/synchronized_sequential.ML
--- /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;
diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/IsaMakefile
--- 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	\
diff -r 1a5e364584ae -r 5db89f8d44f3 src/Pure/ROOT.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 *)