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);
authorwenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11 ago)
changeset 383558cb265fb12fe
parent 38354 fed4e71a8c0f
child 38356 443fb83a21e8
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);
src/Pure/General/markup.scala
src/Pure/General/position.scala
src/Pure/General/xml_data.scala
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_document.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     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 = 0;
    7.32  
    7.33 -val no_id = "";
    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