src/Pure/PIDE/document.ML
changeset 47340 9bbf7fd96bcd
parent 47339 79bd24497ffd
child 47341 00f6279bb67a
equal deleted inserted replaced
47339:79bd24497ffd 47340:9bbf7fd96bcd
    60 
    60 
    61 type node_header = (string * Thy_Header.header) Exn.result;
    61 type node_header = (string * Thy_Header.header) Exn.result;
    62 type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    62 type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    63 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    63 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    64 
    64 
    65 type exec = exec_id * (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
    65 type exec = (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
    66 val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
    66 val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
    67 
    67 
    68 abstype node = Node of
    68 abstype node = Node of
    69  {touched: bool,
    69  {touched: bool,
    70   header: node_header,
    70   header: node_header,
    71   perspective: perspective,
    71   perspective: perspective,
    72   entries: exec option Entries.T,  (*command entries with excecutions*)
    72   entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    73   last_exec: command_id option,  (*last command with exec state assignment*)
    73   last_exec: command_id option,  (*last command with exec state assignment*)
    74   result: Toplevel.state lazy}
    74   result: Toplevel.state lazy}
    75 and version = Version of node Graph.T  (*development graph wrt. static imports*)
    75 and version = Version of node Graph.T  (*development graph wrt. static imports*)
    76 with
    76 with
    77 
    77 
   354         val initial' = initial andalso
   354         val initial' = initial andalso
   355           (case prev of
   355           (case prev of
   356             NONE => true
   356             NONE => true
   357           | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
   357           | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
   358       in (visible', initial') end;
   358       in (visible', initial') end;
   359     fun get_common ((prev, id), exec) (found, (_, flags)) =
   359     fun get_common ((prev, id), opt_exec) (found, (_, flags)) =
   360       if found then NONE
   360       if found then NONE
   361       else
   361       else
   362         let val found' =
   362         let val found' =
   363           is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id));
   363           (case opt_exec of
       
   364             NONE => true
       
   365           | SOME (exec_id, exec) =>
       
   366               (case lookup_entry node0 id of
       
   367                 NONE => true
       
   368               | SOME (exec_id0, _) => exec_id <> exec_id0));
   364         in SOME (found', (prev, update_flags prev flags)) end;
   369         in SOME (found', (prev, update_flags prev flags)) end;
   365     val (found, (common, flags)) =
   370     val (found, (common, flags)) =
   366       iterate_entries get_common node (false, (NONE, (true, true)));
   371       iterate_entries get_common node (false, (NONE, (true, true)));
   367   in
   372   in
   368     if found then (common, flags)
   373     if found then (common, flags)
   407     val is_required = make_required nodes;
   412     val is_required = make_required nodes;
   408 
   413 
   409     val updated =
   414     val updated =
   410       nodes |> Graph.schedule
   415       nodes |> Graph.schedule
   411         (fn deps => fn (name, node) =>
   416         (fn deps => fn (name, node) =>
   412           if not (is_touched node orelse is_required name)
   417           if is_touched node orelse is_required name then
   413           then Future.value (([], [], []), node)
       
   414           else
       
   415             let
   418             let
   416               val node0 = node_of old_version name;
   419               val node0 = node_of old_version name;
   417               fun init () = init_theory deps node;
   420               fun init () = init_theory deps node;
   418               val bad_init =
   421               val bad_init =
   419                 not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   422                 not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   453                       |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
   456                       |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
   454                       |> set_last_exec last_exec
   457                       |> set_last_exec last_exec
   455                       |> set_result result
   458                       |> set_result result
   456                       |> set_touched false;
   459                       |> set_touched false;
   457                   in ((no_execs, execs, [(name, node')]), node') end)
   460                   in ((no_execs, execs, [(name, node')]), node') end)
   458             end)
   461             end
       
   462           else Future.value (([], [], []), node))
   459       |> Future.joins |> map #1;
   463       |> Future.joins |> map #1;
   460 
   464 
   461     val command_execs =
   465     val command_execs =
   462       map (rpair NONE) (maps #1 updated) @
   466       map (rpair NONE) (maps #1 updated) @
   463       map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   467       map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);