Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);

--- a/src/Pure/PIDE/command.scala	Mon Jul 04 22:11:32 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Jul 04 22:25:33 2011 +0200
@@ -80,10 +80,10 @@
   /* dummy commands */
 
   def unparsed(source: String): Command =
-    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
+    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
 
   def span(toks: List[Token]): Command =
-    new Command(Document.NO_ID, toks)
+    new Command(Document.no_id, toks)
 }
 
 
@@ -97,7 +97,7 @@
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
-  def is_unparsed = id == Document.NO_ID
+  def is_unparsed = id == Document.no_id
 
   def name: String = if (is_command) span.head.content else ""
   override def toString =

--- a/src/Pure/PIDE/document.scala	Mon Jul 04 22:11:32 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jul 04 22:25:33 2011 +0200
@@ -27,7 +27,8 @@
   type Command_ID = ID
   type Exec_ID = ID
 
-  val NO_ID: ID = 0
+  val no_id: ID = 0
+  val new_id = new Counter
 
 
 
@@ -121,7 +122,7 @@
 
   object Version
   {
-    val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
+    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
   }
 
   class Version(val id: Version_ID, val nodes: Map[String, Node])

--- a/src/Pure/System/session.scala	Mon Jul 04 22:11:32 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 04 22:25:33 2011 +0200
@@ -115,8 +115,6 @@
 
   /* global state */
 
-  val new_id = new Counter
-
   @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
@@ -273,7 +271,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, 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 22:11:32 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Jul 04 22:25:33 2011 +0200
@@ -99,7 +99,7 @@
 
   /** text edits **/
 
-  def text_edits(syntax: Outer_Syntax, new_id: Counter, previous: Document.Version,
+  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
       edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */
@@ -159,7 +159,7 @@
               (Some(last), spans1.take(spans1.length - 1))
             else (commands.next(last), spans1)
 
-          val inserted = spans2.map(span => new Command(new_id(), span))
+          val inserted = spans2.map(span => new Command(Document.new_id(), span))
           val new_commands =
             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
           recover_spans(new_commands)
@@ -195,7 +195,7 @@
           doc_edits += (name -> Some(cmd_edits))
           nodes += (name -> new Document.Node(commands2))
       }
-      (doc_edits.toList, new Document.Version(new_id(), nodes))
+      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
     }
   }
 }