renamed create_id to new_id;
authorwenzelm
Sun Aug 15 19:30:11 2010 +0200 (2010-08-15 ago)
changeset 38419f9dc924e54f8
parent 38418 9a7af64d71bb
child 38420 7bdf6c79a2db
renamed create_id to new_id;
src/Pure/PIDE/document.ML
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 15 18:41:23 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 15 19:30:11 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    type command_id = id
     1.5    type exec_id = id
     1.6    val no_id: id
     1.7 -  val create_id: unit -> id
     1.8 +  val new_id: unit -> id
     1.9    val parse_id: string -> id
    1.10    val print_id: id -> string
    1.11    type edit = string * ((command_id * command_id option) list) option
    1.12 @@ -38,7 +38,7 @@
    1.13  local
    1.14    val id_count = Synchronized.var "id" 0;
    1.15  in
    1.16 -  fun create_id () =
    1.17 +  fun new_id () =
    1.18      Synchronized.change_result id_count
    1.19        (fn i =>
    1.20          let val i' = i + 1
    1.21 @@ -243,7 +243,7 @@
    1.22  fun new_exec name (id: command_id) (exec_id, updates, state) =
    1.23    let
    1.24      val exec = the_exec state exec_id;
    1.25 -    val exec_id' = create_id ();
    1.26 +    val exec_id' = new_id ();
    1.27      val tr = Toplevel.put_id (print_id exec_id') (the_command state id);
    1.28      val exec' =
    1.29        Lazy.lazy (fn () =>
     2.1 --- a/src/Pure/System/session.scala	Sun Aug 15 18:41:23 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sun Aug 15 19:30:11 2010 +0200
     2.3 @@ -49,7 +49,7 @@
     2.4    /* unique ids */
     2.5  
     2.6    private var id_count: Document.ID = 0
     2.7 -  def create_id(): Document.ID = synchronized {
     2.8 +  def new_id(): Document.ID = synchronized {
     2.9      require(id_count > java.lang.Long.MIN_VALUE)
    2.10      id_count -= 1
    2.11      id_count
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 18:41:23 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 19:30:11 2010 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4                (Some(last), spans1.take(spans1.length - 1))
     3.5              else (commands.next(last), spans1)
     3.6  
     3.7 -          val inserted = spans2.map(span => new Command(session.create_id(), span))
     3.8 +          val inserted = spans2.map(span => new Command(session.new_id(), span))
     3.9            val new_commands =
    3.10              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    3.11            recover_spans(new_commands)
    3.12 @@ -127,7 +127,7 @@
    3.13          doc_edits += (name -> Some(cmd_edits))
    3.14          nodes += (name -> new Document.Node(commands2))
    3.15        }
    3.16 -      (doc_edits.toList, new Document.Version(session.create_id(), nodes))
    3.17 +      (doc_edits.toList, new Document.Version(session.new_id(), nodes))
    3.18      }
    3.19    }
    3.20  }