# HG changeset patch
# User wenzelm
# Date 1244148773 -7200
# Node ID c23663825e23bc058e2983db6c665370baec60a1
# Parent  b861e58086ab81e9bb8fe508618e136d0c612f99
uniform (short) ids on both sides;

diff -r b861e58086ab -r c23663825e23 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu Jun 04 22:08:20 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu Jun 04 22:52:53 2009 +0200
@@ -24,7 +24,7 @@
 type command_id = string;
 type document_id = string;
 
-fun make_id () = "isabelle:" ^ serial_string ();
+fun make_id () = "i" ^ serial_string ();
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
 fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
diff -r b861e58086ab -r c23663825e23 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:08:20 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 04 22:52:53 2009 +0200
@@ -17,6 +17,12 @@
   val charset = "UTF-8"
 
 
+  /* unique ids */
+
+  private var id_count: BigInt = 0
+  def id(): String = synchronized { id_count += 1; "j" + id_count }
+
+
   /* Isabelle environment settings */
 
   private val environment = System.getenv
diff -r b861e58086ab -r c23663825e23 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Thu Jun 04 22:08:20 2009 +0200
+++ b/src/Pure/System/isar.ML	Thu Jun 04 22:52:53 2009 +0200
@@ -290,7 +290,7 @@
       | NONE =>
           let val id =
             if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
-            else "isabelle:" ^ serial_string ()
+            else "i" ^ serial_string ()
           in (id, Toplevel.put_id id raw_tr) end);
 
     val cmd = make_command (category_of tr, tr, Unprocessed);