more uniform Counter in ML and Scala;
authorwenzelm
Fri Jul 05 23:10:18 2013 +0200 (2013-07-05)
changeset 525374b5941730bd8
parent 52536 3a35ce87a55c
child 52538 64206b5b243c
more uniform Counter in ML and Scala;
src/Pure/Concurrent/counter.ML
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/synchronized_sequential.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/PIDE/document_id.ML
src/Pure/PIDE/document_id.scala
src/Pure/ROOT.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/system_channel.scala
src/Pure/Tools/proof_general.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/counter.ML	Fri Jul 05 23:10:18 2013 +0200
     1.3 @@ -0,0 +1,28 @@
     1.4 +(*  Title:      Pure/Concurrent/counter.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Synchronized counter for unique identifiers > 0.
     1.8 +
     1.9 +NB: ML ticks forwards, JVM ticks backwards.
    1.10 +*)
    1.11 +
    1.12 +signature COUNTER =
    1.13 +sig
    1.14 +  val make: unit -> unit -> int
    1.15 +end;
    1.16 +
    1.17 +structure Counter: COUNTER =
    1.18 +struct
    1.19 +
    1.20 +fun make () =
    1.21 +  let
    1.22 +    val counter = Synchronized.var "counter" (0: int);
    1.23 +    fun next () =
    1.24 +      Synchronized.change_result counter
    1.25 +        (fn i =>
    1.26 +          let val j = i + (1: int)
    1.27 +          in (j, j) end);
    1.28 +  in next end;
    1.29 +
    1.30 +end;
    1.31 +
     2.1 --- a/src/Pure/Concurrent/counter.scala	Fri Jul 05 22:58:24 2013 +0200
     2.2 +++ b/src/Pure/Concurrent/counter.scala	Fri Jul 05 23:10:18 2013 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  object Counter
     2.5  {
     2.6    type ID = Long
     2.7 -  def apply(): Counter = new Counter
     2.8 +  def make(): Counter = new Counter
     2.9  }
    2.10  
    2.11  final class Counter private
     3.1 --- a/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 22:58:24 2013 +0200
     3.2 +++ b/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 23:10:18 2013 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4  
     3.5  (* type request *)
     3.6  
     3.7 -val request_counter = Synchronized.counter ();
     3.8 +val request_counter = Counter.make ();
     3.9  datatype request = Request of int;
    3.10  fun new_request () = Request (request_counter ());
    3.11  
     4.1 --- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 22:58:24 2013 +0200
     4.2 +++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 23:10:18 2013 +0200
     4.3 @@ -13,7 +13,6 @@
     4.4    val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
     4.5    val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
     4.6    val change: 'a var -> ('a -> 'a) -> unit
     4.7 -  val counter: unit -> unit -> int
     4.8  end;
     4.9  
    4.10  structure Synchronized: SYNCHRONIZED =
    4.11 @@ -66,18 +65,4 @@
    4.12  
    4.13  end;
    4.14  
    4.15 -
    4.16 -(* unique identifiers > 0 *)
    4.17 -
    4.18 -(*NB: ML ticks forwards, JVM ticks backwards*)
    4.19 -fun counter () =
    4.20 -  let
    4.21 -    val counter = var "counter" (0: int);
    4.22 -    fun next () =
    4.23 -      change_result counter
    4.24 -        (fn i =>
    4.25 -          let val j = i + (1: int)
    4.26 -          in (j, j) end);
    4.27 -  in next end;
    4.28 -
    4.29  end;
     5.1 --- a/src/Pure/Concurrent/synchronized_sequential.ML	Fri Jul 05 22:58:24 2013 +0200
     5.2 +++ b/src/Pure/Concurrent/synchronized_sequential.ML	Fri Jul 05 23:10:18 2013 +0200
     5.3 @@ -25,14 +25,4 @@
     5.4  
     5.5  end;
     5.6  
     5.7 -fun counter () =
     5.8 -  let
     5.9 -    val counter = var "counter" (0: int);
    5.10 -    fun next () =
    5.11 -      change_result counter
    5.12 -        (fn i =>
    5.13 -          let val j = i + (1: int)
    5.14 -          in (j, j) end);
    5.15 -  in next end;
    5.16 -
    5.17  end;
     6.1 --- a/src/Pure/Concurrent/task_queue.ML	Fri Jul 05 22:58:24 2013 +0200
     6.2 +++ b/src/Pure/Concurrent/task_queue.ML	Fri Jul 05 23:10:18 2013 +0200
     6.3 @@ -47,7 +47,7 @@
     6.4  structure Task_Queue: TASK_QUEUE =
     6.5  struct
     6.6  
     6.7 -val new_id = Synchronized.counter ();
     6.8 +val new_id = Counter.make ();
     6.9  
    6.10  
    6.11  (** nested groups of tasks **)
     7.1 --- a/src/Pure/PIDE/document_id.ML	Fri Jul 05 22:58:24 2013 +0200
     7.2 +++ b/src/Pure/PIDE/document_id.ML	Fri Jul 05 23:10:18 2013 +0200
     7.3 @@ -27,7 +27,7 @@
     7.4  type exec = generic;
     7.5  
     7.6  val none = 0;
     7.7 -val make = Synchronized.counter ();
     7.8 +val make = Counter.make ();
     7.9  
    7.10  val parse = Markup.parse_int;
    7.11  val print = Markup.print_int;
     8.1 --- a/src/Pure/PIDE/document_id.scala	Fri Jul 05 22:58:24 2013 +0200
     8.2 +++ b/src/Pure/PIDE/document_id.scala	Fri Jul 05 23:10:18 2013 +0200
     8.3 @@ -17,7 +17,7 @@
     8.4    type Exec = Generic
     8.5  
     8.6    val none: Generic = 0
     8.7 -  val make = Counter()
     8.8 +  val make = Counter.make()
     8.9  
    8.10    def apply(id: Generic): String = Properties.Value.Long.apply(id)
    8.11    def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
     9.1 --- a/src/Pure/ROOT.ML	Fri Jul 05 22:58:24 2013 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Fri Jul 05 23:10:18 2013 +0200
     9.3 @@ -22,6 +22,7 @@
     9.4  use "Concurrent/synchronized.ML";
     9.5  if Multithreading.available then ()
     9.6  else use "Concurrent/synchronized_sequential.ML";
     9.7 +use "Concurrent/counter.ML";
     9.8  
     9.9  use "General/properties.ML";
    9.10  use "General/output.ML";
    10.1 --- a/src/Pure/System/invoke_scala.ML	Fri Jul 05 22:58:24 2013 +0200
    10.2 +++ b/src/Pure/System/invoke_scala.ML	Fri Jul 05 23:10:18 2013 +0200
    10.3 @@ -19,7 +19,7 @@
    10.4  
    10.5  (* pending promises *)
    10.6  
    10.7 -val new_id = string_of_int o Synchronized.counter ();
    10.8 +val new_id = string_of_int o Counter.make ();
    10.9  
   10.10  val promises =
   10.11    Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
    11.1 --- a/src/Pure/System/system_channel.scala	Fri Jul 05 22:58:24 2013 +0200
    11.2 +++ b/src/Pure/System/system_channel.scala	Fri Jul 05 23:10:18 2013 +0200
    11.3 @@ -31,7 +31,7 @@
    11.4  
    11.5  private object Fifo_Channel
    11.6  {
    11.7 -  private val next_fifo = Counter()
    11.8 +  private val next_fifo = Counter.make()
    11.9  }
   11.10  
   11.11  private class Fifo_Channel extends System_Channel
    12.1 --- a/src/Pure/Tools/proof_general.ML	Fri Jul 05 22:58:24 2013 +0200
    12.2 +++ b/src/Pure/Tools/proof_general.ML	Fri Jul 05 23:10:18 2013 +0200
    12.3 @@ -152,7 +152,7 @@
    12.4    | opt_attr name (SOME value) = attr name value;
    12.5  
    12.6  val pgip_id = "dummy";
    12.7 -val pgip_serial = Synchronized.counter ();
    12.8 +val pgip_serial = Counter.make ();
    12.9  
   12.10  fun output_pgip refid refseq content =
   12.11    XML.Elem (("pgip",