tuned;
authorwenzelm
Mon, 29 Jul 2013 15:20:02 +0200
changeset 52771 5009911c7403
parent 52770 8c7cf864e270
child 52772 7764c90680f0
tuned;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jul 29 15:09:20 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 29 15:20:02 2013 +0200
@@ -199,7 +199,7 @@
 type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
 
 val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
-fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
+fun new_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
@@ -226,7 +226,7 @@
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = next_execution version_id;
+      val execution' = new_execution version_id;
     in (versions', commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =