clarified modules;
authorwenzelm
Sat Apr 09 11:21:38 2016 +0200 (2016-04-09)
changeset 629182fcbd4abc021
parent 62917 eed66ba99bd9
child 62919 9eb0359d6a77
clarified modules;
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ROOT.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Concurrent/multithreading.ML	Fri Apr 08 22:48:25 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 11:21:38 2016 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4    val tracing_time: bool -> Time.time -> (unit -> string) -> unit
     1.5    val real_time: ('a -> unit) -> 'a -> Time.time
     1.6    val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
     1.7 -  val serial: unit -> int
     1.8  end;
     1.9  
    1.10  structure Multithreading: MULTITHREADING =
    1.11 @@ -147,24 +146,4 @@
    1.12        val _ = Mutex.unlock lock;
    1.13      in result end) ());
    1.14  
    1.15 -
    1.16 -(* serial numbers *)
    1.17 -
    1.18 -local
    1.19 -
    1.20 -val serial_lock = Mutex.mutex ();
    1.21 -val serial_count = ref 0;
    1.22 -
    1.23 -in
    1.24 -
    1.25 -val serial = uninterruptible (fn _ => fn () =>
    1.26 -  let
    1.27 -    val _ = Mutex.lock serial_lock;
    1.28 -    val _ = serial_count := ! serial_count + 1;
    1.29 -    val res = ! serial_count;
    1.30 -    val _ = Mutex.unlock serial_lock;
    1.31 -  in res end);
    1.32 -
    1.33  end;
    1.34 -
    1.35 -end;
     2.1 --- a/src/Pure/Concurrent/synchronized.ML	Fri Apr 08 22:48:25 2016 +0200
     2.2 +++ b/src/Pure/Concurrent/synchronized.ML	Sat Apr 09 11:21:38 2016 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4          end;
     2.5      in try_change () end);
     2.6  
     2.7 -fun guarded_access var f = the (timed_access var (K NONE) f);
     2.8 +fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
     2.9  
    2.10  
    2.11  (* unconditional change *)
    2.12 @@ -66,9 +66,4 @@
    2.13  
    2.14  end;
    2.15  
    2.16 -
    2.17 -(* toplevel pretty printing *)
    2.18 -
    2.19 -val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
    2.20 -
    2.21  end;
     3.1 --- a/src/Pure/ML/ml_compiler0.ML	Fri Apr 08 22:48:25 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 09 11:21:38 2016 +0200
     3.3 @@ -156,3 +156,5 @@
     3.4           ("addOverload", "ML_system_overload")]))
     3.5      {debug = false, file = "", line = 0, verbose = false}
     3.6      "open PolyML RunCall";
     3.7 +
     3.8 +ML_system_pp (fn depth => fn pretty => fn var => pretty (Synchronized.value var, depth));
     4.1 --- a/src/Pure/ROOT.ML	Fri Apr 08 22:48:25 2016 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Sat Apr 09 11:21:38 2016 +0200
     4.3 @@ -10,9 +10,12 @@
     4.4  ML_file "System/distribution.ML";
     4.5  
     4.6  ML_file "General/exn.ML";
     4.7 +ML_file "General/basics.ML";
     4.8  
     4.9  ML_file "Concurrent/multithreading.ML";
    4.10  ML_file "Concurrent/unsynchronized.ML";
    4.11 +ML_file "Concurrent/synchronized.ML";
    4.12 +ML_file "Concurrent/counter.ML";
    4.13  
    4.14  ML_file "ML/ml_heap.ML";
    4.15  ML_file "ML/ml_profiling.ML";
    4.16 @@ -26,15 +29,11 @@
    4.17  
    4.18  subsection "Library of general tools";
    4.19  
    4.20 -ML_file "General/basics.ML";
    4.21  ML_file "library.ML";
    4.22  ML_file "General/print_mode.ML";
    4.23  ML_file "General/alist.ML";
    4.24  ML_file "General/table.ML";
    4.25  
    4.26 -ML_file "Concurrent/synchronized.ML";
    4.27 -ML_file "Concurrent/counter.ML";
    4.28 -
    4.29  ML_file "General/random.ML";
    4.30  ML_file "General/properties.ML";
    4.31  ML_file "General/output.ML";
     5.1 --- a/src/Pure/library.ML	Fri Apr 08 22:48:25 2016 +0200
     5.2 +++ b/src/Pure/library.ML	Sat Apr 09 11:21:38 2016 +0200
     5.3 @@ -986,7 +986,7 @@
     5.4  (* serial numbers and abstract stamps *)
     5.5  
     5.6  type serial = int;
     5.7 -val serial = Multithreading.serial;
     5.8 +val serial = Counter.make ();
     5.9  val serial_string = string_of_int o serial;
    5.10  
    5.11  datatype stamp = Stamp of serial;