1.1 --- a/src/Pure/Concurrent/par_list_dummy.ML	Thu Oct 01 18:10:41 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,16 +0,0 @@
     1.4 -(*  Title:      Pure/Concurrent/par_list_dummy.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Dummy version of parallel list combinators -- plain sequential evaluation.
     1.8 -*)
     1.9 -
    1.10 -structure Par_List: PAR_LIST =
    1.11 -struct
    1.12 -
    1.13 -val map = map;
    1.14 -val get_some = get_first;
    1.15 -val find_some = find_first;
    1.16 -val exists = exists;
    1.17 -val forall = forall;
    1.18 -
    1.19 -end;

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Concurrent/par_list_sequential.ML	Thu Oct 01 18:21:11 2009 +0200
     2.3 @@ -0,0 +1,16 @@
     2.4 +(*  Title:      Pure/Concurrent/par_list_sequential.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Dummy version of parallel list combinators -- plain sequential evaluation.
     2.8 +*)
     2.9 +
    2.10 +structure Par_List: PAR_LIST =
    2.11 +struct
    2.12 +
    2.13 +val map = map;
    2.14 +val get_some = get_first;
    2.15 +val find_some = find_first;
    2.16 +val exists = exists;
    2.17 +val forall = forall;
    2.18 +
    2.19 +end;

     3.1 --- a/src/Pure/Concurrent/synchronized_dummy.ML	Thu Oct 01 18:10:41 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,25 +0,0 @@
     3.4 -(*  Title:      Pure/Concurrent/synchronized_dummy.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Dummy version of state variables -- plain refs for sequential access.
     3.8 -*)
     3.9 -
    3.10 -structure Synchronized: SYNCHRONIZED =
    3.11 -struct
    3.12 -
    3.13 -datatype 'a var = Var of 'a Unsynchronized.ref;
    3.14 -
    3.15 -fun var _ x = Var (Unsynchronized.ref x);
    3.16 -fun value (Var var) = ! var;
    3.17 -
    3.18 -fun timed_access (Var var) _ f =
    3.19 -  (case f (! var) of
    3.20 -    SOME (y, x') => (var := x'; SOME y)
    3.21 -  | NONE => Thread.unavailable ());
    3.22 -
    3.23 -fun guarded_access var f = the (timed_access var (K NONE) f);
    3.24 -
    3.25 -fun change_result var f = guarded_access var (SOME o f);
    3.26 -fun change var f = change_result var (fn x => ((), f x));
    3.27 -
    3.28 -end;

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 01 18:21:11 2009 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +(*  Title:      Pure/Concurrent/synchronized_sequential.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Sequential version of state variables -- plain refs.
     4.8 +*)
     4.9 +
    4.10 +structure Synchronized: SYNCHRONIZED =
    4.11 +struct
    4.12 +
    4.13 +abstype 'a var = Var of 'a Unsynchronized.ref
    4.14 +with
    4.15 +
    4.16 +fun var _ x = Var (Unsynchronized.ref x);
    4.17 +fun value (Var var) = ! var;
    4.18 +
    4.19 +fun timed_access (Var var) _ f =
    4.20 +  (case f (! var) of
    4.21 +    SOME (y, x') => (var := x'; SOME y)
    4.22 +  | NONE => Thread.unavailable ());
    4.23 +
    4.24 +fun guarded_access var f = the (timed_access var (K NONE) f);
    4.25 +
    4.26 +fun change_result var f = guarded_access var (SOME o f);
    4.27 +fun change var f = change_result var (fn x => ((), f x));
    4.28 +
    4.29 +end;
    4.30 +end;

     5.1 --- a/src/Pure/IsaMakefile	Thu Oct 01 18:10:41 2009 +0200
     5.2 +++ b/src/Pure/IsaMakefile	Thu Oct 01 18:21:11 2009 +0200
     5.3 @@ -45,8 +45,8 @@
     5.4  $(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML			\
     5.5    Concurrent/lazy.ML Concurrent/lazy_sequential.ML			\
     5.6    Concurrent/mailbox.ML Concurrent/par_list.ML				\
     5.7 -  Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
     5.8 -  Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML		\
     5.9 +  Concurrent/par_list_sequential.ML Concurrent/simple_thread.ML		\
    5.10 +  Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML	\
    5.11    Concurrent/task_queue.ML General/alist.ML General/antiquote.ML	\
    5.12    General/balanced_tree.ML General/basics.ML General/binding.ML		\
    5.13    General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\

     6.1 --- a/src/Pure/ROOT.ML	Thu Oct 01 18:10:41 2009 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Thu Oct 01 18:21:11 2009 +0200
     6.3 @@ -57,8 +57,8 @@
     6.4  
     6.5  use "Concurrent/simple_thread.ML";
     6.6  use "Concurrent/synchronized.ML";
     6.7 -if Multithreading.available then () else
     6.8 -use "Concurrent/synchronized_dummy.ML";
     6.9 +if Multithreading.available then ()
    6.10 +else use "Concurrent/synchronized_sequential.ML";
    6.11  use "Concurrent/mailbox.ML";
    6.12  use "Concurrent/task_queue.ML";
    6.13  use "Concurrent/future.ML";
    6.14 @@ -67,7 +67,7 @@
    6.15  else use "Concurrent/lazy_sequential.ML";
    6.16  use "Concurrent/par_list.ML";
    6.17  if Multithreading.available then ()
    6.18 -else use "Concurrent/par_list_dummy.ML";
    6.19 +else use "Concurrent/par_list_sequential.ML";
    6.20  
    6.21  
    6.22  (* fundamental structures *)