# HG changeset patch
# User wenzelm
# Date 1281559286 -7200
# Node ID 8cb265fb12fe5328ada78e5dcc8d585665318ef3
# Parent  fed4e71a8c0f2729b9f7481dd38ffd02ff559c9a
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);

diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -14,6 +14,20 @@
   def get_string(name: String, props: List[(String, String)]): Option[String] =
     props.find(p => p._1 == name).map(_._2)
 
+
+  def parse_long(s: String): Option[Long] =
+    try { Some(java.lang.Long.parseLong(s)) }
+    catch { case _: NumberFormatException => None }
+
+  def get_long(name: String, props: List[(String, String)]): Option[Long] =
+  {
+    get_string(name, props) match {
+      case None => None
+      case Some(value) => parse_long(value)
+    }
+  }
+
+
   def parse_int(s: String): Option[Int] =
     try { Some(Integer.parseInt(s)) }
     catch { case _: NumberFormatException => None }
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/General/position.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -18,7 +18,7 @@
   def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
   def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
   def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
-  def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
+  def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
 
   def get_range(pos: T): Option[(Int, Int)] =
     (get_offset(pos), get_end_offset(pos)) match {
@@ -27,6 +27,6 @@
       case (None, _) => None
     }
 
-  object Id { def unapply(pos: T): Option[String] = get_id(pos) }
+  object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
   object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
 }
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/General/xml_data.scala
--- a/src/Pure/General/xml_data.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/General/xml_data.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -15,6 +15,13 @@
   class XML_Atom(s: String) extends Exception(s)
 
 
+  private def make_long_atom(i: Long): String = i.toString
+
+  private def dest_long_atom(s: String): Long =
+    try { java.lang.Long.parseLong(s) }
+    catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+
   private def make_int_atom(i: Int): String = i.toString
 
   private def dest_int_atom(s: String): Int =
@@ -71,6 +78,9 @@
     }
 
 
+  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
+  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
+
   def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
   def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
 
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Wed Aug 11 22:41:26 2010 +0200
@@ -20,18 +20,17 @@
     Synchronized.change_result id_count
       (fn i =>
         let val i' = i + 1
-        in ("i" ^ string_of_int i', i') end);
+        in (i', i') end);
 end;
 
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
-
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
 
 
 (** documents **)
 
 datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
-type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
+type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
 type document = node Graph.T;   (*development graph via static imports*)
 
 
@@ -40,11 +39,11 @@
 fun make_entry next state = Entry {next = next, state = state};
 
 fun the_entry (node: node) (id: Document.command_id) =
-  (case Symtab.lookup node id of
+  (case Inttab.lookup node id of
     NONE => err_undef "command entry" id
   | SOME (Entry entry) => entry);
 
-fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
+fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
 
 fun put_entry_state (id: Document.command_id) state (node: node) =
   let val {next, ...} = the_entry node id
@@ -62,7 +61,7 @@
       | apply (SOME id) x =
           let val entry = the_entry node id
           in apply (#next entry) (f (id, entry) x) end;
-  in if Symtab.defined node id0 then apply (SOME id0) else I end;
+  in if Inttab.defined node id0 then apply (SOME id0) else I end;
 
 fun first_entry P (node: node) =
   let
@@ -85,7 +84,7 @@
 fun delete_after (id: Document.command_id) (node: node) =
   let val {next, state} = the_entry node id in
     (case next of
-      NONE => error ("No next entry to delete: " ^ quote id)
+      NONE => error ("No next entry to delete: " ^ Document.print_id id)
     | SOME id2 =>
         node |>
           (case #next (the_entry node id2) of
@@ -96,7 +95,7 @@
 
 (* node operations *)
 
-val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
+val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
 
 fun the_node (document: document) name =
   Graph.get_node document name handle Graph.UNDEF _ => empty_node;
@@ -118,17 +117,17 @@
 local
 
 val global_states =
-  Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
+  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
 
 in
 
 fun define_state (id: Document.state_id) state =
   NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_states (Symtab.update_new (id, state))
-      handle Symtab.DUP dup => err_dup "state" dup);
+    Unsynchronized.change global_states (Inttab.update_new (id, state))
+      handle Inttab.DUP dup => err_dup "state" dup);
 
 fun the_state (id: Document.state_id) =
-  (case Symtab.lookup (! global_states) id of
+  (case Inttab.lookup (! global_states) id of
     NONE => err_undef "state" id
   | SOME state => state);
 
@@ -139,23 +138,24 @@
 
 local
 
-val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
+val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
 
 in
 
 fun define_command (id: Document.command_id) text =
   let
+    val id_string = Document.print_id id;
     val tr =
-      Position.setmp_thread_data (Position.id_only id) (fn () =>
-        Outer_Syntax.prepare_command (Position.id id) text) ();
+      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
+        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   in
     NAMED_CRITICAL "Isar" (fn () =>
-      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
-        handle Symtab.DUP dup => err_dup "command" dup)
+      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
+        handle Inttab.DUP dup => err_dup "command" dup)
   end;
 
 fun the_command (id: Document.command_id) =
-  (case Symtab.lookup (! global_commands) id of
+  (case Inttab.lookup (! global_commands) id of
     NONE => err_undef "command" id
   | SOME tr => tr);
 
@@ -166,17 +166,17 @@
 
 local
 
-val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
+val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
 
 in
 
 fun define_document (id: Document.version_id) document =
   NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_documents (Symtab.update_new (id, document))
-      handle Symtab.DUP dup => err_dup "document" dup);
+    Unsynchronized.change global_documents (Inttab.update_new (id, document))
+      handle Inttab.DUP dup => err_dup "document" dup);
 
 fun the_document (id: Document.version_id) =
-  (case Symtab.lookup (! global_documents) id of
+  (case Inttab.lookup (! global_documents) id of
     NONE => err_undef "document" id
   | SOME document => document);
 
@@ -230,7 +230,7 @@
   let
     val state = the_state state_id;
     val state_id' = create_id ();
-    val tr = Toplevel.put_id state_id' (the_command id);
+    val tr = Toplevel.put_id (Document.print_id state_id') (the_command id);
     val state' =
       Lazy.lazy (fn () =>
         (case Lazy.force state of
@@ -240,14 +240,15 @@
   in (state_id', (id, state_id') :: updates) end;
 
 fun updates_status updates =
-  implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+  implode (map (fn (id, state_id) =>
+    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates)
   |> Markup.markup Markup.assign
   |> Output.status;
 
 in
 
 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
-  Position.setmp_thread_data (Position.id_only new_id) (fn () =>
+  Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) (fn () =>
     NAMED_CRITICAL "Isar" (fn () =>
       let
         val old_document = the_document old_id;
@@ -281,16 +282,16 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.define_command"
-    (fn [id, text] => define_command id text);
+    (fn [id, text] => define_command (Document.parse_id id) text);
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_document"
     (fn [old_id, new_id, edits] =>
-      edit_document old_id new_id
+      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
         (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
             (XML_Data.dest_option (XML_Data.dest_list
-                (XML_Data.dest_pair XML_Data.dest_string
-                  (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
+                (XML_Data.dest_pair XML_Data.dest_int
+                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
 
 end;
 
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -23,7 +23,10 @@
     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
       msg match {
         case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
-          Some(cmd_id, state_id)
+          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
+            case (Some(i), Some(j)) => Some((i, j))
+            case _ => None
+          }
         case _ => None
       }
   }
@@ -38,7 +41,7 @@
   /* commands */
 
   def define_command(id: Document.Command_ID, text: String): Unit =
-    input("Isar_Document.define_command", id, text)
+    input("Isar_Document.define_command", Document.print_id(id), text)
 
 
   /* documents */
@@ -47,13 +50,15 @@
       edits: List[Document.Edit[Document.Command_ID]])
   {
     def make_id1(id1: Option[Document.Command_ID]): XML.Body =
-      XML_Data.make_string(id1 getOrElse Document.NO_ID)
+      XML_Data.make_long(id1 getOrElse Document.NO_ID)
+
     val arg =
       XML_Data.make_list(
         XML_Data.make_pair(XML_Data.make_string)(
           XML_Data.make_option(XML_Data.make_list(
-              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
+              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
 
-    input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
+    input("Isar_Document.edit_document",
+      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
   }
 }
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -31,7 +31,7 @@
   }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
-    command_id: Option[String], offset: Option[Int])
+    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
 }
 
 class Command(
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 11 22:41:26 2010 +0200
@@ -7,10 +7,12 @@
 
 signature DOCUMENT =
 sig
-  type state_id = string
-  type command_id = string
-  type version_id = string
-  val no_id: string
+  type state_id = int
+  type command_id = int
+  type version_id = int
+  val no_id: int
+  val parse_id: string -> int
+  val print_id: int -> string
   type edit = string * ((command_id * command_id option) list) option
 end;
 
@@ -19,11 +21,18 @@
 
 (* unique identifiers *)
 
-type state_id = string;
-type command_id = string;
-type version_id = string;
+type state_id = int;
+type command_id = int;
+type version_id = int;
+
+val no_id = 0;
 
-val no_id = "";
+fun parse_id s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise Fail ("Bad id: " ^ quote s));
+
+val print_id = signed_string_of_int;
 
 
 (* edits *)
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -16,11 +16,14 @@
 {
   /* formal identifiers */
 
-  type Version_ID = String
-  type Command_ID = String
-  type State_ID = String
+  type Version_ID = Long
+  type Command_ID = Long
+  type State_ID = Long
 
-  val NO_ID = ""
+  val NO_ID = 0L
+
+  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
+  def print_id(id: Long): String = id.toString
 
 
 
diff -r fed4e71a8c0f -r 8cb265fb12fe src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 11 22:41:26 2010 +0200
@@ -23,7 +23,7 @@
 
   /* managed entities */
 
-  type Entity_ID = String
+  type Entity_ID = Long
 
   trait Entity
   {
@@ -58,8 +58,12 @@
 
   /* unique ids */
 
-  private var id_count: BigInt = 0
-  def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
+  private var id_count: Long = 0
+  def create_id(): Session.Entity_ID = synchronized {
+    require(id_count > java.lang.Long.MIN_VALUE)
+    id_count -= 1
+    id_count
+  }