# HG changeset patch
# User wenzelm
# Date 1281893411 -7200
# Node ID f9dc924e54f81cc94c0c6b8e27dbc9e8c6e12922
# Parent  9a7af64d71bbdfc99c19bb6082d19332de8cc7eb
renamed create_id to new_id;

diff -r 9a7af64d71bb -r f9dc924e54f8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Aug 15 18:41:23 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Aug 15 19:30:11 2010 +0200
@@ -12,7 +12,7 @@
   type command_id = id
   type exec_id = id
   val no_id: id
-  val create_id: unit -> id
+  val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
   type edit = string * ((command_id * command_id option) list) option
@@ -38,7 +38,7 @@
 local
   val id_count = Synchronized.var "id" 0;
 in
-  fun create_id () =
+  fun new_id () =
     Synchronized.change_result id_count
       (fn i =>
         let val i' = i + 1
@@ -243,7 +243,7 @@
 fun new_exec name (id: command_id) (exec_id, updates, state) =
   let
     val exec = the_exec state exec_id;
-    val exec_id' = create_id ();
+    val exec_id' = new_id ();
     val tr = Toplevel.put_id (print_id exec_id') (the_command state id);
     val exec' =
       Lazy.lazy (fn () =>
diff -r 9a7af64d71bb -r f9dc924e54f8 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Aug 15 18:41:23 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 15 19:30:11 2010 +0200
@@ -49,7 +49,7 @@
   /* unique ids */
 
   private var id_count: Document.ID = 0
-  def create_id(): Document.ID = synchronized {
+  def new_id(): Document.ID = synchronized {
     require(id_count > java.lang.Long.MIN_VALUE)
     id_count -= 1
     id_count
diff -r 9a7af64d71bb -r f9dc924e54f8 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 18:41:23 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 19:30:11 2010 +0200
@@ -96,7 +96,7 @@
               (Some(last), spans1.take(spans1.length - 1))
             else (commands.next(last), spans1)
 
-          val inserted = spans2.map(span => new Command(session.create_id(), span))
+          val inserted = spans2.map(span => new Command(session.new_id(), span))
           val new_commands =
             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
           recover_spans(new_commands)
@@ -127,7 +127,7 @@
         doc_edits += (name -> Some(cmd_edits))
         nodes += (name -> new Document.Node(commands2))
       }
-      (doc_edits.toList, new Document.Version(session.create_id(), nodes))
+      (doc_edits.toList, new Document.Version(session.new_id(), nodes))
     }
   }
 }