explicit class Counter;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.scala	Mon Jul 04 20:18:19 2011 +0200
@@ -0,0 +1,27 @@
+/*  Title:      Pure/Concurrent/counter.scala
+    Author:     Makarius
+
+Synchronized counter for unique identifiers < 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*/
+
+package isabelle
+
+
+object Counter
+{
+  type ID = Long
+}
+
+class Counter
+{
+  private var count: Counter.ID = 0
+
+  def apply(): Counter.ID = synchronized {
+    require(count > java.lang.Long.MIN_VALUE)
+    count -= 1
+    count
+  }
+}
+

--- a/src/Pure/System/isabelle_system.scala	Mon Jul 04 16:54:58 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Jul 04 20:18:19 2011 +0200
@@ -257,18 +257,13 @@
 
   /* named pipes */
 
-  private var fifo_count: Long = 0
-  private def next_fifo(): String = synchronized {
-    require(fifo_count < java.lang.Long.MAX_VALUE)
-    fifo_count += 1
-    fifo_count.toString
-  }
+  private val next_fifo = new Counter
 
   def mk_fifo(): String =
   {
     val i = next_fifo()
     val script =
-      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
+      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
       "echo -n \"$FIFO\"\n" +
       "mkfifo -m 600 \"$FIFO\"\n"
     val (out, err, rc) = bash(script)

--- a/src/Pure/System/session.scala	Mon Jul 04 16:54:58 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 04 20:18:19 2011 +0200
@@ -64,17 +64,6 @@
   val assignments = new Event_Bus[Session.Assignment.type]
 
 
-  /* unique ids */
-
-  private var id_count: Document.ID = 0
-  def new_id(): Document.ID = synchronized {
-    require(id_count > java.lang.Long.MIN_VALUE)
-    id_count -= 1
-    id_count
-  }
-
-
-
   /** buffered command changes (delay_first discipline) **/
 
   private case object Stop
@@ -126,6 +115,8 @@
 
   /* global state */
 
+  val new_id = new Counter
+
   @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
@@ -283,7 +274,7 @@
     {
       val previous = global_state.peek().history.tip.version
       val syntax = current_syntax()
-      val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
+      val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id, previous.join, edits) }
       val change = global_state.change_yield(_.extend_history(previous, edits, result))
 
       change.version.map(_ => {

--- a/src/Pure/Thy/thy_syntax.scala	Mon Jul 04 16:54:58 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Jul 04 20:18:19 2011 +0200
@@ -99,7 +99,7 @@
 
   /** text edits **/
 
-  def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version,
+  def text_edits(syntax: Outer_Syntax, new_id: Counter, previous: Document.Version,
       edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */

--- a/src/Pure/build-jars	Mon Jul 04 16:54:58 2011 +0200
+++ b/src/Pure/build-jars	Mon Jul 04 20:18:19 2011 +0200
@@ -9,6 +9,7 @@
 ## sources
 
 declare -a SOURCES=(
+  Concurrent/counter.scala
   Concurrent/future.scala
   Concurrent/simple_thread.scala
   Concurrent/volatile.scala