src/Pure/PIDE/document.ML
changeset 47405 559b44b5164c
parent 47404 e6e5750f1311
child 47406 8818f54773cc
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 09 17:22:23 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 09 17:38:39 2012 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4                      val (common, (visible, initial)) = last_common state last_visible node0 node;
     1.5                      val common_command_exec = the_default_entry node common;
     1.6  
     1.7 -                    val (execs, (command_id, (_, exec)), _) =
     1.8 +                    val (new_execs, (command_id', (_, exec')), _) =
     1.9                        ([], common_command_exec, if initial then SOME init else NONE) |>
    1.10                        (visible orelse required) ?
    1.11                          iterate_entries_after common
    1.12 @@ -510,20 +510,20 @@
    1.13                        iterate_entries_after common
    1.14                          (fn ((_, id0), exec0) => fn res =>
    1.15                            if is_none exec0 then NONE
    1.16 -                          else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
    1.17 +                          else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
    1.18                            else SOME (id0 :: res)) node0 [];
    1.19  
    1.20 -                    val last_exec = if command_id = no_id then NONE else SOME command_id;
    1.21 +                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
    1.22                      val result =
    1.23                        if is_some (after_entry node last_exec) then no_exec
    1.24 -                      else exec;
    1.25 +                      else exec';
    1.26  
    1.27                      val node' = node
    1.28                        |> fold reset_entry no_execs
    1.29 -                      |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
    1.30 +                      |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
    1.31                        |> set_result result
    1.32                        |> set_touched false;
    1.33 -                  in ((no_execs, execs, [(name, node')]), node') end)
    1.34 +                  in ((no_execs, new_execs, [(name, node')]), node') end)
    1.35              end
    1.36            else Future.value (([], [], []), node))
    1.37        |> Future.joins |> map #1;