src/Pure/PIDE/document.ML
changeset 44643 9987ae55e17b
parent 44614 466ea227e00d
child 44644 317e4962dd0f
equal deleted inserted replaced
44642:446fe2abe252 44643:9987ae55e17b
   110     (touched, header, make_perspective ids, entries, last_exec, result));
   110     (touched, header, make_perspective ids, entries, last_exec, result));
   111 
   111 
   112 fun map_entries f =
   112 fun map_entries f =
   113   map_node (fn (touched, header, perspective, entries, last_exec, result) =>
   113   map_node (fn (touched, header, perspective, entries, last_exec, result) =>
   114     (touched, header, perspective, f entries, last_exec, result));
   114     (touched, header, perspective, f entries, last_exec, result));
   115 fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
   115 fun get_entries (Node {entries, ...}) = entries;
       
   116 fun iterate_entries start f = Entries.iterate start f o get_entries;
   116 
   117 
   117 fun get_last_exec (Node {last_exec, ...}) = last_exec;
   118 fun get_last_exec (Node {last_exec, ...}) = last_exec;
   118 fun set_last_exec last_exec =
   119 fun set_last_exec last_exec =
   119   map_node (fn (touched, header, perspective, entries, _, result) =>
   120   map_node (fn (touched, header, perspective, entries, _, result) =>
   120     (touched, header, perspective, entries, last_exec, result));
   121     (touched, header, perspective, entries, last_exec, result));
   181 
   182 
   182 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
   183 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
   183 
   184 
   184 fun touch_node name nodes =
   185 fun touch_node name nodes =
   185   fold (fn desc =>
   186   fold (fn desc =>
   186       update_node desc (set_touched true) #>
   187       update_node desc
   187       desc <> name ? update_node desc (map_entries (reset_after NONE)))
   188         (set_touched true #>
       
   189           desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
   188     (Graph.all_succs nodes [name]) nodes;
   190     (Graph.all_succs nodes [name]) nodes;
   189 
   191 
   190 in
   192 in
   191 
   193 
   192 fun edit_nodes (name, node_edit) (Version nodes) =
   194 fun edit_nodes (name, node_edit) (Version nodes) =
   389     fun get_common ((prev, id), exec) (found, (_, visible)) =
   391     fun get_common ((prev, id), exec) (found, (_, visible)) =
   390       if found then NONE
   392       if found then NONE
   391       else
   393       else
   392         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   394         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   393         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   395         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   394   in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
   396     val (found, (common, visible)) = iterate_entries NONE get_common node (false, (NONE, true));
       
   397     val common' = if found then common else Entries.get_after (get_entries node) common;
       
   398     val visible' = visible andalso common' <> last_visible;
       
   399   in (common', visible') end;
   395 
   400 
   396 fun new_exec state init command_id' (execs, exec) =
   401 fun new_exec state init command_id' (execs, exec) =
   397   let
   402   let
   398     val command' = the_command state command_id';
   403     val command' = the_command state command_id';
   399     val exec_id' = new_id ();
   404     val exec_id' = new_id ();