uniform (short) ids on both sides;
authorwenzelm
Thu Jun 04 22:52:53 2009 +0200 (2009-06-04)
changeset 31443c23663825e23
parent 31442 b861e58086ab
child 31444 4fa98c1df7ba
uniform (short) ids on both sides;
src/Pure/Isar/isar_document.ML
src/Pure/System/isabelle_system.scala
src/Pure/System/isar.ML
     1.1 --- a/src/Pure/Isar/isar_document.ML	Thu Jun 04 22:08:20 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.ML	Thu Jun 04 22:52:53 2009 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  type command_id = string;
     1.5  type document_id = string;
     1.6  
     1.7 -fun make_id () = "isabelle:" ^ serial_string ();
     1.8 +fun make_id () = "i" ^ serial_string ();
     1.9  
    1.10  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    1.11  fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
     2.1 --- a/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:08:20 2009 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:52:53 2009 +0200
     2.3 @@ -17,6 +17,12 @@
     2.4    val charset = "UTF-8"
     2.5  
     2.6  
     2.7 +  /* unique ids */
     2.8 +
     2.9 +  private var id_count: BigInt = 0
    2.10 +  def id(): String = synchronized { id_count += 1; "j" + id_count }
    2.11 +
    2.12 +
    2.13    /* Isabelle environment settings */
    2.14  
    2.15    private val environment = System.getenv
     3.1 --- a/src/Pure/System/isar.ML	Thu Jun 04 22:08:20 2009 +0200
     3.2 +++ b/src/Pure/System/isar.ML	Thu Jun 04 22:52:53 2009 +0200
     3.3 @@ -290,7 +290,7 @@
     3.4        | NONE =>
     3.5            let val id =
     3.6              if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
     3.7 -            else "isabelle:" ^ serial_string ()
     3.8 +            else "i" ^ serial_string ()
     3.9            in (id, Toplevel.put_id id raw_tr) end);
    3.10  
    3.11      val cmd = make_command (category_of tr, tr, Unprocessed);