tuned;
authorwenzelm
Mon Jul 29 15:20:02 2013 +0200 (2013-07-29 ago)
changeset 527715009911c7403
parent 52770 8c7cf864e270
child 52772 7764c90680f0
tuned;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 15:09:20 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 15:20:02 2013 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
     1.5  
     1.6  val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
     1.7 -fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
     1.8 +fun new_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
     1.9  
    1.10  abstype state = State of
    1.11   {versions: version Inttab.table,  (*version id -> document content*)
    1.12 @@ -226,7 +226,7 @@
    1.13      let
    1.14        val versions' = Inttab.update_new (version_id, version) versions
    1.15          handle Inttab.DUP dup => err_dup "document version" dup;
    1.16 -      val execution' = next_execution version_id;
    1.17 +      val execution' = new_execution version_id;
    1.18      in (versions', commands, execution') end);
    1.19  
    1.20  fun the_version (State {versions, ...}) version_id =