1.1 --- a/src/Pure/General/markup.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -14,6 +14,20 @@
     1.4    def get_string(name: String, props: List[(String, String)]): Option[String] =
     1.5      props.find(p => p._1 == name).map(_._2)
     1.6  
     1.7 +
     1.8 +  def parse_long(s: String): Option[Long] =
     1.9 +    try { Some(java.lang.Long.parseLong(s)) }
    1.10 +    catch { case _: NumberFormatException => None }
    1.11 +
    1.12 +  def get_long(name: String, props: List[(String, String)]): Option[Long] =
    1.13 +  {
    1.14 +    get_string(name, props) match {
    1.15 +      case None => None
    1.16 +      case Some(value) => parse_long(value)
    1.17 +    }
    1.18 +  }
    1.19 +
    1.20 +
    1.21    def parse_int(s: String): Option[Int] =
    1.22      try { Some(Integer.parseInt(s)) }
    1.23      catch { case _: NumberFormatException => None }

     2.1 --- a/src/Pure/General/position.scala	Wed Aug 11 18:44:06 2010 +0200
     2.2 +++ b/src/Pure/General/position.scala	Wed Aug 11 22:41:26 2010 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
     2.5    def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
     2.6    def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
     2.7 -  def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
     2.8 +  def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
     2.9  
    2.10    def get_range(pos: T): Option[(Int, Int)] =
    2.11      (get_offset(pos), get_end_offset(pos)) match {
    2.12 @@ -27,6 +27,6 @@
    2.13        case (None, _) => None
    2.14      }
    2.15  
    2.16 -  object Id { def unapply(pos: T): Option[String] = get_id(pos) }
    2.17 +  object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    2.18    object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
    2.19  }

     3.1 --- a/src/Pure/General/xml_data.scala	Wed Aug 11 18:44:06 2010 +0200
     3.2 +++ b/src/Pure/General/xml_data.scala	Wed Aug 11 22:41:26 2010 +0200
     3.3 @@ -15,6 +15,13 @@
     3.4    class XML_Atom(s: String) extends Exception(s)
     3.5  
     3.6  
     3.7 +  private def make_long_atom(i: Long): String = i.toString
     3.8 +
     3.9 +  private def dest_long_atom(s: String): Long =
    3.10 +    try { java.lang.Long.parseLong(s) }
    3.11 +    catch { case e: NumberFormatException => throw new XML_Atom(s) }
    3.12 +
    3.13 +
    3.14    private def make_int_atom(i: Int): String = i.toString
    3.15  
    3.16    private def dest_int_atom(s: String): Int =
    3.17 @@ -71,6 +78,9 @@
    3.18      }
    3.19  
    3.20  
    3.21 +  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
    3.22 +  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
    3.23 +
    3.24    def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
    3.25    def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
    3.26  

     4.1 --- a/src/Pure/Isar/isar_document.ML	Wed Aug 11 18:44:06 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_document.ML	Wed Aug 11 22:41:26 2010 +0200
     4.3 @@ -20,18 +20,17 @@
     4.4      Synchronized.change_result id_count
     4.5        (fn i =>
     4.6          let val i' = i + 1
     4.7 -        in ("i" ^ string_of_int i', i') end);
     4.8 +        in (i', i') end);
     4.9  end;
    4.10  
    4.11 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    4.12 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
    4.13 -
    4.14 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
    4.15 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
    4.16  
    4.17  
    4.18  (** documents **)
    4.19  
    4.20  datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
    4.21 -type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
    4.22 +type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    4.23  type document = node Graph.T;   (*development graph via static imports*)
    4.24  
    4.25  
    4.26 @@ -40,11 +39,11 @@
    4.27  fun make_entry next state = Entry {next = next, state = state};
    4.28  
    4.29  fun the_entry (node: node) (id: Document.command_id) =
    4.30 -  (case Symtab.lookup node id of
    4.31 +  (case Inttab.lookup node id of
    4.32      NONE => err_undef "command entry" id
    4.33    | SOME (Entry entry) => entry);
    4.34  
    4.35 -fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
    4.36 +fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    4.37  
    4.38  fun put_entry_state (id: Document.command_id) state (node: node) =
    4.39    let val {next, ...} = the_entry node id
    4.40 @@ -62,7 +61,7 @@
    4.41        | apply (SOME id) x =
    4.42            let val entry = the_entry node id
    4.43            in apply (#next entry) (f (id, entry) x) end;
    4.44 -  in if Symtab.defined node id0 then apply (SOME id0) else I end;
    4.45 +  in if Inttab.defined node id0 then apply (SOME id0) else I end;
    4.46  
    4.47  fun first_entry P (node: node) =
    4.48    let
    4.49 @@ -85,7 +84,7 @@
    4.50  fun delete_after (id: Document.command_id) (node: node) =
    4.51    let val {next, state} = the_entry node id in
    4.52      (case next of
    4.53 -      NONE => error ("No next entry to delete: " ^ quote id)
    4.54 +      NONE => error ("No next entry to delete: " ^ Document.print_id id)
    4.55      | SOME id2 =>
    4.56          node |>
    4.57            (case #next (the_entry node id2) of
    4.58 @@ -96,7 +95,7 @@
    4.59  
    4.60  (* node operations *)
    4.61  
    4.62 -val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    4.63 +val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    4.64  
    4.65  fun the_node (document: document) name =
    4.66    Graph.get_node document name handle Graph.UNDEF _ => empty_node;
    4.67 @@ -118,17 +117,17 @@
    4.68  local
    4.69  
    4.70  val global_states =
    4.71 -  Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
    4.72 +  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
    4.73  
    4.74  in
    4.75  
    4.76  fun define_state (id: Document.state_id) state =
    4.77    NAMED_CRITICAL "Isar" (fn () =>
    4.78 -    Unsynchronized.change global_states (Symtab.update_new (id, state))
    4.79 -      handle Symtab.DUP dup => err_dup "state" dup);
    4.80 +    Unsynchronized.change global_states (Inttab.update_new (id, state))
    4.81 +      handle Inttab.DUP dup => err_dup "state" dup);
    4.82  
    4.83  fun the_state (id: Document.state_id) =
    4.84 -  (case Symtab.lookup (! global_states) id of
    4.85 +  (case Inttab.lookup (! global_states) id of
    4.86      NONE => err_undef "state" id
    4.87    | SOME state => state);
    4.88  
    4.89 @@ -139,23 +138,24 @@
    4.90  
    4.91  local
    4.92  
    4.93 -val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
    4.94 +val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
    4.95  
    4.96  in
    4.97  
    4.98  fun define_command (id: Document.command_id) text =
    4.99    let
   4.100 +    val id_string = Document.print_id id;
   4.101      val tr =
   4.102 -      Position.setmp_thread_data (Position.id_only id) (fn () =>
   4.103 -        Outer_Syntax.prepare_command (Position.id id) text) ();
   4.104 +      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
   4.105 +        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   4.106    in
   4.107      NAMED_CRITICAL "Isar" (fn () =>
   4.108 -      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   4.109 -        handle Symtab.DUP dup => err_dup "command" dup)
   4.110 +      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
   4.111 +        handle Inttab.DUP dup => err_dup "command" dup)
   4.112    end;
   4.113  
   4.114  fun the_command (id: Document.command_id) =
   4.115 -  (case Symtab.lookup (! global_commands) id of
   4.116 +  (case Inttab.lookup (! global_commands) id of
   4.117      NONE => err_undef "command" id
   4.118    | SOME tr => tr);
   4.119  
   4.120 @@ -166,17 +166,17 @@
   4.121  
   4.122  local
   4.123  
   4.124 -val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
   4.125 +val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
   4.126  
   4.127  in
   4.128  
   4.129  fun define_document (id: Document.version_id) document =
   4.130    NAMED_CRITICAL "Isar" (fn () =>
   4.131 -    Unsynchronized.change global_documents (Symtab.update_new (id, document))
   4.132 -      handle Symtab.DUP dup => err_dup "document" dup);
   4.133 +    Unsynchronized.change global_documents (Inttab.update_new (id, document))
   4.134 +      handle Inttab.DUP dup => err_dup "document" dup);
   4.135  
   4.136  fun the_document (id: Document.version_id) =
   4.137 -  (case Symtab.lookup (! global_documents) id of
   4.138 +  (case Inttab.lookup (! global_documents) id of
   4.139      NONE => err_undef "document" id
   4.140    | SOME document => document);
   4.141  
   4.142 @@ -230,7 +230,7 @@
   4.143    let
   4.144      val state = the_state state_id;
   4.145      val state_id' = create_id ();
   4.146 -    val tr = Toplevel.put_id state_id' (the_command id);
   4.147 +    val tr = Toplevel.put_id (Document.print_id state_id') (the_command id);
   4.148      val state' =
   4.149        Lazy.lazy (fn () =>
   4.150          (case Lazy.force state of
   4.151 @@ -240,14 +240,15 @@
   4.152    in (state_id', (id, state_id') :: updates) end;
   4.153  
   4.154  fun updates_status updates =
   4.155 -  implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   4.156 +  implode (map (fn (id, state_id) =>
   4.157 +    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates)
   4.158    |> Markup.markup Markup.assign
   4.159    |> Output.status;
   4.160  
   4.161  in
   4.162  
   4.163  fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   4.164 -  Position.setmp_thread_data (Position.id_only new_id) (fn () =>
   4.165 +  Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) (fn () =>
   4.166      NAMED_CRITICAL "Isar" (fn () =>
   4.167        let
   4.168          val old_document = the_document old_id;
   4.169 @@ -281,16 +282,16 @@
   4.170  
   4.171  val _ =
   4.172    Isabelle_Process.add_command "Isar_Document.define_command"
   4.173 -    (fn [id, text] => define_command id text);
   4.174 +    (fn [id, text] => define_command (Document.parse_id id) text);
   4.175  
   4.176  val _ =
   4.177    Isabelle_Process.add_command "Isar_Document.edit_document"
   4.178      (fn [old_id, new_id, edits] =>
   4.179 -      edit_document old_id new_id
   4.180 +      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   4.181          (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   4.182              (XML_Data.dest_option (XML_Data.dest_list
   4.183 -                (XML_Data.dest_pair XML_Data.dest_string
   4.184 -                  (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
   4.185 +                (XML_Data.dest_pair XML_Data.dest_int
   4.186 +                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
   4.187  
   4.188  end;
   4.189  

     5.1 --- a/src/Pure/Isar/isar_document.scala	Wed Aug 11 18:44:06 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_document.scala	Wed Aug 11 22:41:26 2010 +0200
     5.3 @@ -23,7 +23,10 @@
     5.4      def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
     5.5        msg match {
     5.6          case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
     5.7 -          Some(cmd_id, state_id)
     5.8 +          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
     5.9 +            case (Some(i), Some(j)) => Some((i, j))
    5.10 +            case _ => None
    5.11 +          }
    5.12          case _ => None
    5.13        }
    5.14    }
    5.15 @@ -38,7 +41,7 @@
    5.16    /* commands */
    5.17  
    5.18    def define_command(id: Document.Command_ID, text: String): Unit =
    5.19 -    input("Isar_Document.define_command", id, text)
    5.20 +    input("Isar_Document.define_command", Document.print_id(id), text)
    5.21  
    5.22  
    5.23    /* documents */
    5.24 @@ -47,13 +50,15 @@
    5.25        edits: List[Document.Edit[Document.Command_ID]])
    5.26    {
    5.27      def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    5.28 -      XML_Data.make_string(id1 getOrElse Document.NO_ID)
    5.29 +      XML_Data.make_long(id1 getOrElse Document.NO_ID)
    5.30 +
    5.31      val arg =
    5.32        XML_Data.make_list(
    5.33          XML_Data.make_pair(XML_Data.make_string)(
    5.34            XML_Data.make_option(XML_Data.make_list(
    5.35 -              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
    5.36 +              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    5.37  
    5.38 -    input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
    5.39 +    input("Isar_Document.edit_document",
    5.40 +      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
    5.41    }
    5.42  }

     6.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 11 18:44:06 2010 +0200
     6.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 11 22:41:26 2010 +0200
     6.3 @@ -31,7 +31,7 @@
     6.4    }
     6.5    case class TypeInfo(ty: String)
     6.6    case class RefInfo(file: Option[String], line: Option[Int],
     6.7 -    command_id: Option[String], offset: Option[Int])
     6.8 +    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
     6.9  }
    6.10  
    6.11  class Command(

     7.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 11 18:44:06 2010 +0200
     7.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 11 22:41:26 2010 +0200
     7.3 @@ -7,10 +7,12 @@
     7.4  
     7.5  signature DOCUMENT =
     7.6  sig
     7.7 -  type state_id = string
     7.8 -  type command_id = string
     7.9 -  type version_id = string
    7.10 -  val no_id: string
    7.11 +  type state_id = int
    7.12 +  type command_id = int
    7.13 +  type version_id = int
    7.14 +  val no_id: int
    7.15 +  val parse_id: string -> int
    7.16 +  val print_id: int -> string
    7.17    type edit = string * ((command_id * command_id option) list) option
    7.18  end;
    7.19  
    7.20 @@ -19,11 +21,18 @@
    7.21  
    7.22  (* unique identifiers *)
    7.23  
    7.24 -type state_id = string;
    7.25 -type command_id = string;
    7.26 -type version_id = string;
    7.27 +type state_id = int;
    7.28 +type command_id = int;
    7.29 +type version_id = int;
    7.30  
    7.31 -val no_id = "";
    7.32 +val no_id = 0;
    7.33 +
    7.34 +fun parse_id s =
    7.35 +  (case Int.fromString s of
    7.36 +    SOME i => i
    7.37 +  | NONE => raise Fail ("Bad id: " ^ quote s));
    7.38 +
    7.39 +val print_id = signed_string_of_int;
    7.40  
    7.41  
    7.42  (* edits *)

     8.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 11 18:44:06 2010 +0200
     8.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 11 22:41:26 2010 +0200
     8.3 @@ -16,11 +16,14 @@
     8.4  {
     8.5    /* formal identifiers */
     8.6  
     8.7 -  type Version_ID = String
     8.8 -  type Command_ID = String
     8.9 -  type State_ID = String
    8.10 +  type Version_ID = Long
    8.11 +  type Command_ID = Long
    8.12 +  type State_ID = Long
    8.13  
    8.14 -  val NO_ID = ""
    8.15 +  val NO_ID = 0L
    8.16 +
    8.17 +  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
    8.18 +  def print_id(id: Long): String = id.toString
    8.19  
    8.20  
    8.21  

     9.1 --- a/src/Pure/System/session.scala	Wed Aug 11 18:44:06 2010 +0200
     9.2 +++ b/src/Pure/System/session.scala	Wed Aug 11 22:41:26 2010 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4  
     9.5    /* managed entities */
     9.6  
     9.7 -  type Entity_ID = String
     9.8 +  type Entity_ID = Long
     9.9  
    9.10    trait Entity
    9.11    {
    9.12 @@ -58,8 +58,12 @@
    9.13  
    9.14    /* unique ids */
    9.15  
    9.16 -  private var id_count: BigInt = 0
    9.17 -  def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
    9.18 +  private var id_count: Long = 0
    9.19 +  def create_id(): Session.Entity_ID = synchronized {
    9.20 +    require(id_count > java.lang.Long.MIN_VALUE)
    9.21 +    id_count -= 1
    9.22 +    id_count
    9.23 +  }
    9.24  
    9.25  
    9.26