src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -75,7 +75,7 @@
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
-    def + (alt_id: Document.ID, message: XML.Elem): State =
+    def + (alt_id: Document_ID.ID, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -136,7 +136,7 @@
   type Span = List[Token]
 
   def apply(
-    id: Document.Command_ID,
+    id: Document_ID.Command,
     node_name: Document.Node.Name,
     span: Span,
     results: Results = Results.empty,
@@ -160,16 +160,16 @@
     new Command(id, node_name, span1.toList, source, results, markup)
   }
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
 
-  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
     Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
 
   def unparsed(source: String): Command =
-    unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
+    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
 
-  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
+  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
   {
     val text = XML.content(body)
     val markup = Markup_Tree.from_XML(body)
@@ -200,7 +200,7 @@
 
 
 final class Command private(
-    val id: Document.Command_ID,
+    val id: Document_ID.Command,
     val node_name: Document.Node.Name,
     val span: Command.Span,
     val source: String,
@@ -209,7 +209,7 @@
 {
   /* classification */
 
-  def is_undefined: Boolean = id == Document.no_id
+  def is_undefined: Boolean = id == Document_ID.none
   val is_unparsed: Boolean = span.exists(_.is_unparsed)
   val is_unfinished: Boolean = span.exists(_.is_unfinished)