# HG changeset patch
# User wenzelm
# Date 1460193698 -7200
# Node ID 2fcbd4abc021f76d447584e2a79848048975e853
# Parent  eed66ba99bd995b5d04df44214405511b94da438
clarified modules;

diff -r eed66ba99bd9 -r 2fcbd4abc021 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 11:21:38 2016 +0200
@@ -23,7 +23,6 @@
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
-  val serial: unit -> int
 end;
 
 structure Multithreading: MULTITHREADING =
@@ -147,24 +146,4 @@
       val _ = Mutex.unlock lock;
     in result end) ());
 
-
-(* serial numbers *)
-
-local
-
-val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
-
-in
-
-val serial = uninterruptible (fn _ => fn () =>
-  let
-    val _ = Mutex.lock serial_lock;
-    val _ = serial_count := ! serial_count + 1;
-    val res = ! serial_count;
-    val _ = Mutex.unlock serial_lock;
-  in res end);
-
 end;
-
-end;
diff -r eed66ba99bd9 -r 2fcbd4abc021 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Sat Apr 09 11:21:38 2016 +0200
@@ -56,7 +56,7 @@
         end;
     in try_change () end);
 
-fun guarded_access var f = the (timed_access var (K NONE) f);
+fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
 
 
 (* unconditional change *)
@@ -66,9 +66,4 @@
 
 end;
 
-
-(* toplevel pretty printing *)
-
-val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
-
 end;
diff -r eed66ba99bd9 -r 2fcbd4abc021 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 09 11:21:38 2016 +0200
@@ -156,3 +156,5 @@
          ("addOverload", "ML_system_overload")]))
     {debug = false, file = "", line = 0, verbose = false}
     "open PolyML RunCall";
+
+ML_system_pp (fn depth => fn pretty => fn var => pretty (Synchronized.value var, depth));
diff -r eed66ba99bd9 -r 2fcbd4abc021 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 09 11:21:38 2016 +0200
@@ -10,9 +10,12 @@
 ML_file "System/distribution.ML";
 
 ML_file "General/exn.ML";
+ML_file "General/basics.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
+ML_file "Concurrent/synchronized.ML";
+ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_profiling.ML";
@@ -26,15 +29,11 @@
 
 subsection "Library of general tools";
 
-ML_file "General/basics.ML";
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 
-ML_file "Concurrent/synchronized.ML";
-ML_file "Concurrent/counter.ML";
-
 ML_file "General/random.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
diff -r eed66ba99bd9 -r 2fcbd4abc021 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/library.ML	Sat Apr 09 11:21:38 2016 +0200
@@ -986,7 +986,7 @@
 (* serial numbers and abstract stamps *)
 
 type serial = int;
-val serial = Multithreading.serial;
+val serial = Counter.make ();
 val serial_string = string_of_int o serial;
 
 datatype stamp = Stamp of serial;