src/Pure/PIDE/document.ML
changeset 44446 f9334afb6945
parent 44445 364fd07398f5
child 44476 e8a87398f35d
equal deleted inserted replaced
44445:364fd07398f5 44446:f9334afb6945
    91   map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
    91   map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
    92 
    92 
    93 
    93 
    94 (* basic components *)
    94 (* basic components *)
    95 
    95 
    96 fun get_touched (Node {touched, ...}) = touched;
    96 fun is_touched (Node {touched, ...}) = touched;
    97 fun set_touched touched =
    97 fun set_touched touched =
    98   map_node (fn (_, header, perspective, entries, result) =>
    98   map_node (fn (_, header, perspective, entries, result) =>
    99     (touched, header, perspective, entries, result));
    99     (touched, header, perspective, entries, result));
   100 
   100 
   101 fun get_header (Node {header, ...}) = header;
   101 fun get_header (Node {header, ...}) = header;
   403     val new_version = fold edit_nodes edits old_version;
   403     val new_version = fold edit_nodes edits old_version;
   404 
   404 
   405     val updates =
   405     val updates =
   406       nodes_of new_version |> Graph.schedule
   406       nodes_of new_version |> Graph.schedule
   407         (fn deps => fn (name, node) =>
   407         (fn deps => fn (name, node) =>
   408           if not (get_touched node) then Future.value (([], [], []), node)
   408           if not (is_touched node) then Future.value (([], [], []), node)
   409           else
   409           else
   410             (case first_entry NONE (is_changed (node_of old_version name)) node of
   410             (case first_entry NONE (is_changed (node_of old_version name)) node of
   411               NONE => Future.value (([], [], []), set_touched false node)
   411               NONE => Future.value (([], [], []), set_touched false node)
   412             | SOME ((prev, id), _) =>
   412             | SOME ((prev, id), _) =>
   413                 let
   413                 let