src/Pure/PIDE/document.ML
changeset 44544 da5f0af32c1b
parent 44483 383a5b9efbd0
child 44610 49657380fba6
equal deleted inserted replaced
44543:ba8f24f7156e 44544:da5f0af32c1b
   213             (header, Graph.add_deps_acyclic (name, parents) nodes2)
   213             (header, Graph.add_deps_acyclic (name, parents) nodes2)
   214               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
   214               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
   215         in Graph.map_node name (set_header header') nodes3 end
   215         in Graph.map_node name (set_header header') nodes3 end
   216         |> touch_node name
   216         |> touch_node name
   217     | Perspective perspective =>
   217     | Perspective perspective =>
   218         nodes
   218         update_node name (set_perspective perspective) nodes);
   219         |> update_node name (set_perspective perspective)
       
   220         |> touch_node name (* FIXME more precise!?! *));
       
   221 
   219 
   222 end;
   220 end;
   223 
   221 
   224 fun put_node (name, node) (Version nodes) =
   222 fun put_node (name, node) (Version nodes) =
   225   Version (update_node name (K node) nodes);
   223   Version (update_node name (K node) nodes);
   380 
   378 
   381 local
   379 local
   382 
   380 
   383 fun last_common last_visible node0 node =
   381 fun last_common last_visible node0 node =
   384   let
   382   let
   385     fun get_common ((prev, id), exec) (found, (result, visible)) =
   383     fun get_common ((prev, id), exec) (found, (_, visible)) =
   386       if found then NONE
   384       if found then NONE
   387       else
   385       else
   388         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   386         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   389         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   387         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   390   in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
   388   in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
   401           |> Toplevel.put_id (print_id exec_id');
   399           |> Toplevel.put_id (print_id exec_id');
   402         in run_command tr st end)
   400         in run_command tr st end)
   403       |> pair command_id';
   401       |> pair command_id';
   404   in ((exec_id', exec') :: execs, exec') end;
   402   in ((exec_id', exec') :: execs, exec') end;
   405 
   403 
       
   404 fun make_required nodes =
       
   405   let
       
   406     val all_visible =
       
   407       Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
       
   408       |> Graph.all_preds nodes;
       
   409     val required =
       
   410       fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
       
   411         all_visible Symtab.empty;
       
   412   in Symtab.defined required end;
       
   413 
   406 fun init_theory deps name node =
   414 fun init_theory deps name node =
   407   let
   415   let
   408     val (thy_name, imports, uses) = Exn.release (get_header node);
   416     val (thy_name, imports, uses) = Exn.release (get_header node);
   409     (* FIXME provide files via Scala layer *)
   417     (* FIXME provide files via Scala layer *)
   410     val (dir, files) =
   418     val (dir, files) =
   426   let
   434   let
   427     val old_version = the_version state old_id;
   435     val old_version = the_version state old_id;
   428     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   436     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   429     val new_version = fold edit_nodes edits old_version;
   437     val new_version = fold edit_nodes edits old_version;
   430 
   438 
       
   439     val nodes = nodes_of new_version;
       
   440     val is_required = make_required nodes;
       
   441 
   431     val updated =
   442     val updated =
   432       nodes_of new_version |> Graph.schedule
   443       nodes |> Graph.schedule
   433         (fn deps => fn (name, node) =>
   444         (fn deps => fn (name, node) =>
   434           if not (is_touched node) then Future.value (([], [], []), node)
   445           if not (is_touched node orelse is_required name)
       
   446           then Future.value (([], [], []), node)
   435           else
   447           else
   436             let
   448             let
   437               val node0 = node_of old_version name;
   449               val node0 = node_of old_version name;
   438               fun init () = init_theory deps name node;
   450               fun init () = init_theory deps name node;
   439             in
   451             in
   440               (singleton o Future.forks)
   452               (singleton o Future.forks)
   441                 {name = "Document.update", group = NONE,
   453                 {name = "Document.update", group = NONE,
   442                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   454                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   443                 (fn () =>
   455                 (fn () =>
   444                   let
   456                   let
       
   457                     val required = is_required name;
   445                     val last_visible = #2 (get_perspective node);
   458                     val last_visible = #2 (get_perspective node);
   446                     val (common, visible) = last_common last_visible node0 node;
   459                     val (common, visible) = last_common last_visible node0 node;
   447                     val common_exec = the_exec state (the_default_entry node common);
   460                     val common_exec = the_exec state (the_default_entry node common);
   448 
   461 
   449                     val (execs, exec) = ([], common_exec) |>
   462                     val (execs, exec) = ([], common_exec) |>
   450                       visible ?
   463                       (visible orelse required) ?
   451                         iterate_entries (after_entry node common)
   464                         iterate_entries (after_entry node common)
   452                           (fn ((prev, id), _) => fn res =>
   465                           (fn ((prev, id), _) => fn res =>
   453                             if prev = last_visible then NONE
   466                             if not required andalso prev = last_visible then NONE
   454                             else SOME (new_exec state init id res)) node;
   467                             else SOME (new_exec state init id res)) node;
   455 
   468 
   456                     val no_execs =
   469                     val no_execs =
   457                       iterate_entries (after_entry node0 common)
   470                       iterate_entries (after_entry node0 common)
   458                         (fn ((_, id0), exec0) => fn res =>
   471                         (fn ((_, id0), exec0) => fn res =>