src/Pure/PIDE/document.ML
changeset 70284 3e17c3a5fd39
parent 70283 9ebbb53f4b50
child 70610 d14ddb1df52c
     1.1 --- a/src/Pure/PIDE/document.ML	Sun May 19 14:14:56 2019 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun May 19 18:10:45 2019 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val remove_versions: Document_ID.version list -> state -> state
     1.5    val start_execution: state -> state
     1.6    val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     1.7 -    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
     1.8 +    string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
     1.9    val state: unit -> state
    1.10    val change_state: (state -> state) -> unit
    1.11  end;
    1.12 @@ -869,7 +869,7 @@
    1.13      val state' = state
    1.14        |> define_version new_version_id new_version assigned_nodes;
    1.15  
    1.16 -  in (removed, assign_result, state') end);
    1.17 +  in (Symtab.keys edited, removed, assign_result, state') end);
    1.18  
    1.19  end;
    1.20