src/Pure/PIDE/document.ML
changeset 70284 3e17c3a5fd39
parent 70283 9ebbb53f4b50
child 70610 d14ddb1df52c
--- a/src/Pure/PIDE/document.ML	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Sun May 19 18:10:45 2019 +0200
@@ -25,7 +25,7 @@
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
-    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
+    string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -869,7 +869,7 @@
     val state' = state
       |> define_version new_version_id new_version assigned_nodes;
 
-  in (removed, assign_result, state') end);
+  in (Symtab.keys edited, removed, assign_result, state') end);
 
 end;