--- 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 () =>
--- 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
--- 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))
}
}
}