more uniform Counter in ML and Scala;

--- /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",