amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
authorwenzelm
Thu Sep 01 23:08:42 2011 +0200 (2011-09-01 ago)
changeset 446439987ae55e17b
parent 44642 446fe2abe252
child 44644 317e4962dd0f
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
clarified touch_node: reset result explicitly;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Sep 01 22:29:57 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Sep 01 23:08:42 2011 +0200
     1.3 @@ -112,7 +112,8 @@
     1.4  fun map_entries f =
     1.5    map_node (fn (touched, header, perspective, entries, last_exec, result) =>
     1.6      (touched, header, perspective, f entries, last_exec, result));
     1.7 -fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
     1.8 +fun get_entries (Node {entries, ...}) = entries;
     1.9 +fun iterate_entries start f = Entries.iterate start f o get_entries;
    1.10  
    1.11  fun get_last_exec (Node {last_exec, ...}) = last_exec;
    1.12  fun set_last_exec last_exec =
    1.13 @@ -183,8 +184,9 @@
    1.14  
    1.15  fun touch_node name nodes =
    1.16    fold (fn desc =>
    1.17 -      update_node desc (set_touched true) #>
    1.18 -      desc <> name ? update_node desc (map_entries (reset_after NONE)))
    1.19 +      update_node desc
    1.20 +        (set_touched true #>
    1.21 +          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
    1.22      (Graph.all_succs nodes [name]) nodes;
    1.23  
    1.24  in
    1.25 @@ -391,7 +393,10 @@
    1.26        else
    1.27          let val found' = is_none exec orelse exec <> lookup_entry node0 id
    1.28          in SOME (found', (prev, visible andalso prev <> last_visible)) end;
    1.29 -  in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
    1.30 +    val (found, (common, visible)) = iterate_entries NONE get_common node (false, (NONE, true));
    1.31 +    val common' = if found then common else Entries.get_after (get_entries node) common;
    1.32 +    val visible' = visible andalso common' <> last_visible;
    1.33 +  in (common', visible') end;
    1.34  
    1.35  fun new_exec state init command_id' (execs, exec) =
    1.36    let