1.1 --- a/src/Pure/PIDE/command.scala	Mon Jul 04 22:11:32 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Jul 04 22:25:33 2011 +0200
     1.3 @@ -80,10 +80,10 @@
     1.4    /* dummy commands */
     1.5  
     1.6    def unparsed(source: String): Command =
     1.7 -    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
     1.8 +    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
     1.9  
    1.10    def span(toks: List[Token]): Command =
    1.11 -    new Command(Document.NO_ID, toks)
    1.12 +    new Command(Document.no_id, toks)
    1.13  }
    1.14  
    1.15  
    1.16 @@ -97,7 +97,7 @@
    1.17    def is_ignored: Boolean = span.forall(_.is_ignored)
    1.18    def is_malformed: Boolean = !is_command && !is_ignored
    1.19  
    1.20 -  def is_unparsed = id == Document.NO_ID
    1.21 +  def is_unparsed = id == Document.no_id
    1.22  
    1.23    def name: String = if (is_command) span.head.content else ""
    1.24    override def toString =

     2.1 --- a/src/Pure/PIDE/document.scala	Mon Jul 04 22:11:32 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon Jul 04 22:25:33 2011 +0200
     2.3 @@ -27,7 +27,8 @@
     2.4    type Command_ID = ID
     2.5    type Exec_ID = ID
     2.6  
     2.7 -  val NO_ID: ID = 0
     2.8 +  val no_id: ID = 0
     2.9 +  val new_id = new Counter
    2.10  
    2.11  
    2.12  
    2.13 @@ -121,7 +122,7 @@
    2.14  
    2.15    object Version
    2.16    {
    2.17 -    val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
    2.18 +    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
    2.19    }
    2.20  
    2.21    class Version(val id: Version_ID, val nodes: Map[String, Node])

     3.1 --- a/src/Pure/System/session.scala	Mon Jul 04 22:11:32 2011 +0200
     3.2 +++ b/src/Pure/System/session.scala	Mon Jul 04 22:25:33 2011 +0200
     3.3 @@ -115,8 +115,6 @@
     3.4  
     3.5    /* global state */
     3.6  
     3.7 -  val new_id = new Counter
     3.8 -
     3.9    @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
    3.10    def current_syntax(): Outer_Syntax = syntax
    3.11  
    3.12 @@ -273,7 +271,7 @@
    3.13      {
    3.14        val previous = global_state.peek().history.tip.version
    3.15        val syntax = current_syntax()
    3.16 -      val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id, previous.join, edits) }
    3.17 +      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
    3.18        val change = global_state.change_yield(_.extend_history(previous, edits, result))
    3.19  
    3.20        change.version.map(_ => {

     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Jul 04 22:11:32 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Jul 04 22:25:33 2011 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4  
     4.5    /** text edits **/
     4.6  
     4.7 -  def text_edits(syntax: Outer_Syntax, new_id: Counter, previous: Document.Version,
     4.8 +  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
     4.9        edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
    4.10    {
    4.11      /* phase 1: edit individual command source */
    4.12 @@ -159,7 +159,7 @@
    4.13                (Some(last), spans1.take(spans1.length - 1))
    4.14              else (commands.next(last), spans1)
    4.15  
    4.16 -          val inserted = spans2.map(span => new Command(new_id(), span))
    4.17 +          val inserted = spans2.map(span => new Command(Document.new_id(), span))
    4.18            val new_commands =
    4.19              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    4.20            recover_spans(new_commands)
    4.21 @@ -195,7 +195,7 @@
    4.22            doc_edits += (name -> Some(cmd_edits))
    4.23            nodes += (name -> new Document.Node(commands2))
    4.24        }
    4.25 -      (doc_edits.toList, new Document.Version(new_id(), nodes))
    4.26 +      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
    4.27      }
    4.28    }
    4.29  }