# HG changeset patch
# User wenzelm
# Date 1373031483 -7200
# Node ID 99dd8b4ef3fe241fc64338cc50bd297d4078cbb5
# Parent  b6a224676c04e957d112d53305824b92248cdf57
explicit module Document_ID as source of globally unique identifiers across ML/Scala;

diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -69,6 +69,7 @@
 
 (* unique identifiers > 0 *)
 
+(*NB: ML ticks forwards, JVM ticks backwards*)
 fun counter () =
   let
     val counter = var "counter" (0: int);
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -23,8 +23,8 @@
   val no_eval: eval
   val eval: span -> Toplevel.transition -> eval_state -> eval_state
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
-  type print = {name: string, pri: int, exec_id: int, print: unit memo}
-  val print: (unit -> int) -> string -> eval -> print list
+  type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
+  val print: string -> eval -> print list
   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
 end;
 
@@ -175,7 +175,7 @@
 
 (* print *)
 
-type print = {name: string, pri: int, exec_id: int, print: unit memo};
+type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 local
@@ -192,13 +192,13 @@
 
 in
 
-fun print new_id command_name eval =
+fun print command_name eval =
   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
     (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
       Exn.Res NONE => NONE
     | Exn.Res (SOME print_fn) =>
         let
-          val exec_id = new_id ();
+          val exec_id = Document_ID.make ();
           fun body () =
             let
               val {failed, command, state = st', ...} = memo_result eval;
@@ -207,7 +207,7 @@
         in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
     | Exn.Exn exn =>
         let
-          val exec_id = new_id ();
+          val exec_id = Document_ID.make ();
           fun body () =
             let
               val {command, ...} = memo_result eval;
diff -r b6a224676c04 -r 99dd8b4ef3fe 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)
 
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -7,31 +7,23 @@
 
 signature DOCUMENT =
 sig
-  type id = int
-  type version_id = id
-  type command_id = id
-  type exec_id = id
-  val no_id: id
-  val new_id: unit -> id
-  val parse_id: string -> id
-  val print_id: id -> string
   type node_header = string * Thy_Header.header * string list
   datatype node_edit =
     Clear |    (* FIXME unused !? *)
-    Edits of (command_id option * command_id option) list |
+    Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
-    Perspective of command_id list
+    Perspective of Document_ID.command list
   type edit = string * node_edit
   type state
   val init_state: state
-  val define_command: command_id -> string -> string -> state -> state
-  val remove_versions: version_id list -> state -> state
+  val define_command: Document_ID.command -> string -> string -> state -> state
+  val remove_versions: Document_ID.version list -> state -> state
   val discontinue_execution: state -> unit
   val cancel_execution: state -> unit
   val start_execution: state -> unit
   val timing: bool Unsynchronized.ref
-  val update: version_id -> version_id -> edit list -> state ->
-    (command_id * exec_id list) list * state
+  val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
+    (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -39,27 +31,10 @@
 structure Document: DOCUMENT =
 struct
 
-(* unique identifiers *)
-
-type id = int;
-type version_id = id;
-type command_id = id;
-type exec_id = id;
-
-val no_id = 0;
-val new_id = Synchronized.counter ();
-
-val parse_id = Markup.parse_int;
-val print_id = Markup.print_int;
-
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
-
-
 (* command execution *)
 
-type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
-val no_exec: exec = (no_id, (Command.no_eval, []));
+type exec = Document_ID.exec * (Command.eval * Command.print list);  (*eval/print process*)
+val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
 
 fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
 
@@ -74,9 +49,12 @@
 
 (** document structure **)
 
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
+
 type node_header = string * Thy_Header.header * string list;
-type perspective = Inttab.set * command_id option;
-structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+type perspective = Inttab.set * Document_ID.command option;
+structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
@@ -156,9 +134,9 @@
 
 datatype node_edit =
   Clear |
-  Edits of (command_id option * command_id option) list |
+  Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
-  Perspective of command_id list;
+  Perspective of Document_ID.command list;
 
 type edit = string * node_edit;
 
@@ -175,7 +153,7 @@
   | SOME (exec, _) => exec);
 
 fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
-  | the_default_entry _ NONE = (no_id, no_exec);
+  | the_default_entry _ NONE = (Document_ID.none, no_exec);
 
 fun update_entry id exec =
   map_entries (Entries.update (id, exec));
@@ -237,7 +215,8 @@
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
-  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
+  execution:
+    Document_ID.version * Future.group * bool Unsynchronized.ref}  (*current execution process*)
 with
 
 fun make_state (versions, commands, execution) =
@@ -247,15 +226,15 @@
   make_state (f (versions, commands, execution));
 
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
-    (no_id, Future.new_group NONE, Unsynchronized.ref false));
+  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
+    (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
 
 fun execution_of (State {execution, ...}) = execution;
 
 
 (* document versions *)
 
-fun define_version (id: version_id) version =
+fun define_version (id: Document_ID.version) version =
   map_state (fn (versions, commands, _) =>
     let
       val versions' = Inttab.update_new (id, version) versions
@@ -263,21 +242,21 @@
       val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
     in (versions', commands, execution') end);
 
-fun the_version (State {versions, ...}) (id: version_id) =
+fun the_version (State {versions, ...}) (id: Document_ID.version) =
   (case Inttab.lookup versions id of
     NONE => err_undef "document version" id
   | SOME version => version);
 
-fun delete_version (id: version_id) versions = Inttab.delete id versions
+fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
   handle Inttab.UNDEF _ => err_undef "document version" id;
 
 
 (* commands *)
 
-fun define_command (id: command_id) name text =
+fun define_command (id: Document_ID.command) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val id_string = print_id id;
+      val id_string = Document_ID.print id;
       val span = Lazy.lazy (fn () =>
         Position.setmp_thread_data (Position.id_only id_string)
           (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
@@ -290,7 +269,7 @@
           handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, commands', execution) end);
 
-fun the_command (State {commands, ...}) (id: command_id) =
+fun the_command (State {commands, ...}) (id: Document_ID.command) =
   (case Inttab.lookup commands id of
     NONE => err_undef "command" id
   | SOME command => command);
@@ -300,7 +279,7 @@
 fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   let
     val _ = member (op =) ids (#1 execution) andalso
-      error ("Attempt to remove execution version " ^ print_id (#1 execution));
+      error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
 
     val versions' = fold delete_version ids versions;
     val commands' =
@@ -451,19 +430,19 @@
           (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
         else (I, init);
 
-      val exec_id' = new_id ();
+      val exec_id' = Document_ID.make ();
       val eval' =
         Command.memo (fn () =>
           let
             val eval_state = exec_result (snd command_exec);
             val tr =
-              Position.setmp_thread_data (Position.id_only (print_id exec_id'))
+              Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
                 (fn () =>
                   Command.read span
                   |> modify_init
                   |> Toplevel.put_id exec_id') ();
           in Command.eval span tr eval_state end);
-      val prints' = if command_visible then Command.print new_id command_name eval' else [];
+      val prints' = if command_visible then Command.print command_name eval' else [];
       val command_exec' = (command_id', (exec_id', (eval', prints')));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
@@ -472,7 +451,7 @@
     SOME (exec_id, (eval, prints)) =>
       let
         val (command_name, _) = the_command state command_id;
-        val new_prints = Command.print new_id command_name eval;
+        val new_prints = Command.print command_name eval;
         val prints' =
           new_prints |> map (fn new_print =>
             (case find_first (fn {name, ...} => name = #name new_print) prints of
@@ -486,7 +465,7 @@
 
 in
 
-fun update (old_id: version_id) (new_id: version_id) edits state =
+fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
   let
     val old_version = the_version state old_id;
     val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
@@ -547,7 +526,8 @@
                           then SOME res
                           else SOME (id0 :: res)) node0 [];
 
-                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
+                    val last_exec =
+                      if command_id' = Document_ID.none then NONE else SOME command_id';
                     val result =
                       if is_some (after_entry node last_exec) then NONE
                       else SOME eval';
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -13,20 +13,6 @@
 
 object Document
 {
-  /* formal identifiers */
-
-  type ID = Long
-  val ID = Properties.Value.Long
-
-  type Version_ID = ID
-  type Command_ID = ID
-  type Exec_ID = ID
-
-  val no_id: ID = 0
-  val new_id = Counter()
-
-
-
   /** document structure **/
 
   /* individual nodes */
@@ -202,15 +188,15 @@
     val init: Version = new Version()
 
     def make(syntax: Outer_Syntax, nodes: Nodes): Version =
-      new Version(new_id(), syntax, nodes)
+      new Version(Document_ID.make(), syntax, nodes)
   }
 
   final class Version private(
-    val id: Version_ID = no_id,
+    val id: Document_ID.Version = Document_ID.none,
     val syntax: Outer_Syntax = Outer_Syntax.empty,
     val nodes: Nodes = Nodes.empty)
   {
-    def is_init: Boolean = id == no_id
+    def is_init: Boolean = id == Document_ID.none
   }
 
 
@@ -289,7 +275,7 @@
       result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }
 
-  type Assign = List[(Document.Command_ID, List[Document.Exec_ID])]  // exec state assignment
+  type Assign = List[(Document_ID.Command, List[Document_ID.Exec])]  // exec state assignment
 
   object State
   {
@@ -301,13 +287,14 @@
     }
 
     final class Assignment private(
-      val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
+      val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
       val is_finished: Boolean = false)
     {
       def check_finished: Assignment = { require(is_finished); this }
       def unfinished: Assignment = new Assignment(command_execs, false)
 
-      def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
+      def assign(
+        add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
       {
         require(!is_finished)
         val command_execs1 =
@@ -324,10 +311,10 @@
   }
 
   final case class State private(
-    val versions: Map[Version_ID, Version] = Map.empty,
-    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
-    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
-    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
+    val versions: Map[Document_ID.Version, Version] = Map.empty,
+    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
+    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
+    val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -345,9 +332,9 @@
       copy(commands = commands + (id -> command.init_state))
     }
 
-    def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
+    def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: ID): Option[(Node, Command)] =
+    def find_command(version: Version, id: Document_ID.ID): Option[(Node, Command)] =
       commands.get(id) orElse execs.get(id) match {
         case None => None
         case Some(st) =>
@@ -356,13 +343,13 @@
           Some((node, command))
       }
 
-    def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
-    def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
+    def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
+    def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
+    def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
 
-    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
+    def accumulate(id: Document_ID.ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some(st) =>
           val new_st = st + (id, message)
@@ -376,7 +363,7 @@
           }
       }
 
-    def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
+    def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
     {
       val version = the_version(id)
 
@@ -437,12 +424,12 @@
       }
     }
 
-    def removed_versions(removed: List[Version_ID]): State =
+    def removed_versions(removed: List[Document_ID.Version]): State =
     {
       val versions1 = versions -- removed
       val assignments1 = assignments -- removed
-      var commands1 = Map.empty[Command_ID, Command.State]
-      var execs1 = Map.empty[Exec_ID, Command.State]
+      var commands1 = Map.empty[Document_ID.Command, Command.State]
+      var execs1 = Map.empty[Document_ID.Exec, Command.State]
       for {
         (version_id, version) <- versions1.iterator
         command_execs = assignments1(version_id).command_execs
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/document_id.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/PIDE/document_id.ML
+    Author:     Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*)
+
+signature DOCUMENT_ID =
+sig
+  type id = int
+  type version = id
+  type command = id
+  type exec = id
+  val none: id
+  val make: unit -> id
+  val parse: string -> id
+  val print: id -> string
+end;
+
+structure Document_ID: DOCUMENT_ID =
+struct
+
+type id = int;
+type version = id;
+type command = id;
+type exec = id;
+
+val none = 0;
+val make = Synchronized.counter ();
+
+val parse = Markup.parse_int;
+val print = Markup.print_int;
+
+end;
+
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/document_id.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -0,0 +1,24 @@
+/*  Title:      Pure/PIDE/document_id.scala
+    Author:     Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*/
+
+package isabelle
+
+
+object Document_ID
+{
+  type ID = Long
+  val ID = Properties.Value.Long
+
+  type Version = ID
+  type Command = ID
+  type Exec = ID
+
+  val none: ID = 0
+  val make = Counter()
+}
+
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -10,7 +10,7 @@
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
     (fn [id, name, text] =>
-      Document.change_state (Document.define_command (Document.parse_id id) name text));
+      Document.change_state (Document.define_command (Document_ID.parse id) name text));
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
@@ -26,8 +26,8 @@
       let
         val _ = Document.cancel_execution state;
 
-        val old_id = Document.parse_id old_id_string;
-        val new_id = Document.parse_id new_id_string;
+        val old_id = Document_ID.parse old_id_string;
+        val new_id = Document_ID.parse new_id_string;
         val edits =
           YXML.parse_body edits_yxml |>
             let open XML.Decode in
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -13,7 +13,7 @@
 
   object Assign
   {
-    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+    def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
       try {
         import XML.Decode._
         val body = YXML.parse_body(text)
@@ -27,7 +27,7 @@
 
   object Removed
   {
-    def unapply(text: String): Option[List[Document.Version_ID]] =
+    def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
         Some(list(long)(YXML.parse_body(text)))
@@ -86,7 +86,7 @@
 
   object Command_Timing
   {
-    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+    def unapply(props: Properties.T): Option[(Document_ID.ID, isabelle.Timing)] =
       props match {
         case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
           (args, args) match {
@@ -233,7 +233,7 @@
 
   object Dialog_Args
   {
-    def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
+    def unapply(props: Properties.T): Option[(Document_ID.ID, Long, String)] =
       (props, props, props) match {
         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
           Some((id, serial, result))
@@ -243,7 +243,7 @@
 
   object Dialog
   {
-    def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
+    def unapply(tree: XML.Tree): Option[(Document_ID.ID, Long, String)] =
       tree match {
         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
           Some((id, serial, result))
@@ -253,7 +253,7 @@
 
   object Dialog_Result
   {
-    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
+    def apply(id: Document_ID.ID, serial: Long, result: String): XML.Elem =
     {
       val props = Position.Id(id) ::: Markup.Serial(serial)
       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
@@ -309,7 +309,7 @@
 
   def define_command(command: Command): Unit =
     input("Document.define_command",
-      Document.ID(command.id), encode(command.name), encode(command.source))
+      Document_ID.ID(command.id), encode(command.name), encode(command.source))
 
 
   /* document versions */
@@ -318,7 +318,7 @@
 
   def cancel_execution() { input("Document.cancel_execution") }
 
-  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
+  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
   {
     val edits_yxml =
@@ -346,7 +346,7 @@
         pair(string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode_edits(edits)) }
-    input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+    input("Document.update", Document_ID.ID(old_id), Document_ID.ID(new_id), edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/ROOT
--- a/src/Pure/ROOT	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/ROOT	Fri Jul 05 15:38:03 2013 +0200
@@ -152,6 +152,7 @@
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/document.ML"
+    "PIDE/document_id.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
     "PIDE/xml.ML"
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/ROOT.ML	Fri Jul 05 15:38:03 2013 +0200
@@ -265,6 +265,7 @@
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
 use "Thy/present.ML";
+use "PIDE/document_id.ML";
 use "PIDE/command.ML";
 use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/System/session.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -26,7 +26,7 @@
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(edits: List[Document.Edit_Text])
-  case class Dialog_Result(id: Document.ID, serial: Long, result: String)
+  case class Dialog_Result(id: Document_ID.ID, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -374,7 +374,7 @@
           System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
-      def accumulate(state_id: Document.ID, message: XML.Elem)
+      def accumulate(state_id: Document_ID.ID, message: XML.Elem)
       {
         try {
           val st = global_state >>> (_.accumulate(state_id, message))
@@ -548,6 +548,6 @@
   def update_options(options: Options)
   { session_actor !? Update_Options(options) }
 
-  def dialog_result(id: Document.ID, serial: Long, result: String)
+  def dialog_result(id: Document_ID.ID, serial: Long, result: String)
   { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+      spans.foreach(span => add(Command(Document_ID.none, node_name, span)))
       result()
     }
   }
@@ -225,7 +225,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+        val inserted = spans2.map(span => Command(Document_ID.make(), name, span))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/build-jars	Fri Jul 05 15:38:03 2013 +0200
@@ -33,6 +33,7 @@
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala
+  PIDE/document_id.scala
   PIDE/markup.scala
   PIDE/markup_tree.scala
   PIDE/protocol.scala
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -26,7 +26,7 @@
           val buffer = model.buffer
           val snapshot = model.snapshot()
 
-          def try_replace_command(exec_id: Document.ID, s: String)
+          def try_replace_command(exec_id: Document_ID.ID, s: String)
           {
             snapshot.state.execs.get(exec_id).map(_.command) match {
               case Some(command) =>
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -24,7 +24,7 @@
   private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
     formatted_body: XML.Body): (String, Document.State) =
   {
-    val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
+    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
     val node_name = command.node_name
     val edits: List[Document.Edit_Text] =
       List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
@@ -38,7 +38,7 @@
     val state1 =
       state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
         .define_version(version1, state0.the_assignment(version0))
-        .assign(version1.id, List(command.id -> List(Document.new_id())))._2
+        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
 
     (command.source, state1)
   }
diff -r b6a224676c04 -r 99dd8b4ef3fe src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 15:38:03 2013 +0200
@@ -290,7 +290,7 @@
 
           case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
           if !body.isEmpty =>
-            val entry: Command.Results.Entry = (Document.new_id(), msg)
+            val entry: Command.Results.Entry = (Document_ID.make(), msg)
             Text.Info(snapshot.convert(info_range), entry) :: msgs
         }).toList.flatMap(_.info)
     if (results.isEmpty) None