--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.ML Fri Jul 05 23:10:18 2013 +0200
@@ -0,0 +1,28 @@
+(* Title: Pure/Concurrent/counter.ML
+ Author: Makarius
+
+Synchronized counter for unique identifiers > 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*)
+
+signature COUNTER =
+sig
+ val make: unit -> unit -> int
+end;
+
+structure Counter: COUNTER =
+struct
+
+fun make () =
+ let
+ val counter = Synchronized.var "counter" (0: int);
+ fun next () =
+ Synchronized.change_result counter
+ (fn i =>
+ let val j = i + (1: int)
+ in (j, j) end);
+ in next end;
+
+end;
+
--- a/src/Pure/Concurrent/counter.scala Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/counter.scala Fri Jul 05 23:10:18 2013 +0200
@@ -13,7 +13,7 @@
object Counter
{
type ID = Long
- def apply(): Counter = new Counter
+ def make(): Counter = new Counter
}
final class Counter private
--- a/src/Pure/Concurrent/event_timer.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Fri Jul 05 23:10:18 2013 +0200
@@ -26,7 +26,7 @@
(* type request *)
-val request_counter = Synchronized.counter ();
+val request_counter = Counter.make ();
datatype request = Request of int;
fun new_request () = Request (request_counter ());
--- a/src/Pure/Concurrent/synchronized.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Fri Jul 05 23:10:18 2013 +0200
@@ -13,7 +13,6 @@
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
val change: 'a var -> ('a -> 'a) -> unit
- val counter: unit -> unit -> int
end;
structure Synchronized: SYNCHRONIZED =
@@ -66,18 +65,4 @@
end;
-
-(* unique identifiers > 0 *)
-
-(*NB: ML ticks forwards, JVM ticks backwards*)
-fun counter () =
- let
- val counter = var "counter" (0: int);
- fun next () =
- change_result counter
- (fn i =>
- let val j = i + (1: int)
- in (j, j) end);
- in next end;
-
end;
--- a/src/Pure/Concurrent/synchronized_sequential.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Fri Jul 05 23:10:18 2013 +0200
@@ -25,14 +25,4 @@
end;
-fun counter () =
- let
- val counter = var "counter" (0: int);
- fun next () =
- change_result counter
- (fn i =>
- let val j = i + (1: int)
- in (j, j) end);
- in next end;
-
end;
--- a/src/Pure/Concurrent/task_queue.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Fri Jul 05 23:10:18 2013 +0200
@@ -47,7 +47,7 @@
structure Task_Queue: TASK_QUEUE =
struct
-val new_id = Synchronized.counter ();
+val new_id = Counter.make ();
(** nested groups of tasks **)
--- a/src/Pure/PIDE/document_id.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/PIDE/document_id.ML Fri Jul 05 23:10:18 2013 +0200
@@ -27,7 +27,7 @@
type exec = generic;
val none = 0;
-val make = Synchronized.counter ();
+val make = Counter.make ();
val parse = Markup.parse_int;
val print = Markup.print_int;
--- a/src/Pure/PIDE/document_id.scala Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/PIDE/document_id.scala Fri Jul 05 23:10:18 2013 +0200
@@ -17,7 +17,7 @@
type Exec = Generic
val none: Generic = 0
- val make = Counter()
+ val make = Counter.make()
def apply(id: Generic): String = Properties.Value.Long.apply(id)
def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
--- a/src/Pure/ROOT.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 05 23:10:18 2013 +0200
@@ -22,6 +22,7 @@
use "Concurrent/synchronized.ML";
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
+use "Concurrent/counter.ML";
use "General/properties.ML";
use "General/output.ML";
--- a/src/Pure/System/invoke_scala.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/System/invoke_scala.ML Fri Jul 05 23:10:18 2013 +0200
@@ -19,7 +19,7 @@
(* pending promises *)
-val new_id = string_of_int o Synchronized.counter ();
+val new_id = string_of_int o Counter.make ();
val promises =
Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
--- a/src/Pure/System/system_channel.scala Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/System/system_channel.scala Fri Jul 05 23:10:18 2013 +0200
@@ -31,7 +31,7 @@
private object Fifo_Channel
{
- private val next_fifo = Counter()
+ private val next_fifo = Counter.make()
}
private class Fifo_Channel extends System_Channel
--- a/src/Pure/Tools/proof_general.ML Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Fri Jul 05 23:10:18 2013 +0200
@@ -152,7 +152,7 @@
| opt_attr name (SOME value) = attr name value;
val pgip_id = "dummy";
-val pgip_serial = Synchronized.counter ();
+val pgip_serial = Counter.make ();
fun output_pgip refid refseq content =
XML.Elem (("pgip",