src/Pure/PIDE/document.ML
changeset 44645 5938beb84adc
parent 44644 317e4962dd0f
child 44660 90bab3febb6c
equal deleted inserted replaced
44644:317e4962dd0f 44645:5938beb84adc
   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 get_entries (Node {entries, ...}) = entries;
   115 fun get_entries (Node {entries, ...}) = entries;
   116 fun iterate_entries start f = Entries.iterate start f o get_entries;
   116 
       
   117 fun iterate_entries f = Entries.iterate NONE f o get_entries;
       
   118 fun iterate_entries_after start f (Node {entries, ...}) =
       
   119   (case Entries.get_after entries start of
       
   120     NONE => I
       
   121   | SOME id => Entries.iterate (SOME id) f entries);
   117 
   122 
   118 fun get_last_exec (Node {last_exec, ...}) = last_exec;
   123 fun get_last_exec (Node {last_exec, ...}) = last_exec;
   119 fun set_last_exec last_exec =
   124 fun set_last_exec last_exec =
   120   map_node (fn (touched, header, perspective, entries, _, result) =>
   125   map_node (fn (touched, header, perspective, entries, _, result) =>
   121     (touched, header, perspective, entries, last_exec, result));
   126     (touched, header, perspective, entries, last_exec, result));
   345     val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   350     val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   346 
   351 
   347     val _ = Multithreading.interrupted ();
   352     val _ = Multithreading.interrupted ();
   348     val _ = Toplevel.status tr Markup.forked;
   353     val _ = Toplevel.status tr Markup.forked;
   349     val start = Timing.start ();
   354     val start = Timing.start ();
   350     val (errs, result) =
   355     val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   351       if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
       
   352       else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
       
   353     val _ = timing tr (Timing.result start);
   356     val _ = timing tr (Timing.result start);
   354     val _ = Toplevel.status tr Markup.joined;
   357     val _ = Toplevel.status tr Markup.joined;
   355     val _ = List.app (Toplevel.error_msg tr) errs;
   358     val _ = List.app (Toplevel.error_msg tr) errs;
   356   in
   359   in
   357     (case result of
   360     (case result of
   384 
   387 
   385 (* edits *)
   388 (* edits *)
   386 
   389 
   387 local
   390 local
   388 
   391 
   389 fun last_common last_visible node0 node =
   392 fun last_common state last_visible node0 node =
   390   let
   393   let
   391     fun get_common ((prev, id), exec) (found, (_, visible)) =
   394     fun update_flags prev (visible, initial) =
       
   395       let
       
   396         val visible' = visible andalso prev <> last_visible;
       
   397         val initial' = initial andalso
       
   398           (case prev of
       
   399             NONE => true
       
   400           | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
       
   401       in (visible', initial') end;
       
   402     fun get_common ((prev, id), exec) (found, (_, flags)) =
   392       if found then NONE
   403       if found then NONE
   393       else
   404       else
   394         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   405         let val found' = is_none exec orelse exec <> lookup_entry node0 id
   395         in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   406         in SOME (found', (prev, update_flags prev flags)) end;
   396     val (found, (common, visible)) = iterate_entries NONE get_common node (false, (NONE, true));
   407     val (found, (common, flags)) =
   397     val common' = if found then common else Entries.get_after (get_entries node) common;
   408       iterate_entries get_common node (false, (NONE, (true, true)));
   398     val visible' = visible andalso common' <> last_visible;
   409   in
   399   in (common', visible') end;
   410     if found then (common, flags)
   400 
   411     else
   401 fun new_exec state init command_id' (execs, exec) =
   412       let val last = Entries.get_after (get_entries node) common
   402   let
   413       in (last, update_flags last flags) end
   403     val (_, tr0) = the_command state command_id';
   414   end;
   404     val exec_id' = new_id ();
   415 
   405     val exec' =
   416 fun illegal_init () = error "Illegal theory header after end of theory";
   406       snd exec |> Lazy.map (fn (st, _) =>
   417 
   407         let val tr =
   418 fun new_exec state bad_init command_id' (execs, exec, init) =
   408           Future.join tr0
   419   if bad_init andalso is_none init then NONE
   409           |> Toplevel.modify_init init
   420   else
   410           |> Toplevel.put_id (print_id exec_id');
   421     let
   411         in run_command tr st end)
   422       val (name, tr0) = the_command state command_id';
   412       |> pair command_id';
   423       val (modify_init, init') =
   413   in ((exec_id', exec') :: execs, exec') end;
   424         if Keyword.is_theory_begin name then
       
   425           (Toplevel.modify_init (the_default illegal_init init), NONE)
       
   426         else (I, init);
       
   427         val exec_id' = new_id ();
       
   428       val exec' =
       
   429         snd exec |> Lazy.map (fn (st, _) =>
       
   430           let val tr =
       
   431             Future.join tr0
       
   432             |> modify_init
       
   433             |> Toplevel.put_id (print_id exec_id');
       
   434           in run_command tr st end)
       
   435         |> pair command_id';
       
   436     in SOME ((exec_id', exec') :: execs, exec', init') end;
   414 
   437 
   415 fun make_required nodes =
   438 fun make_required nodes =
   416   let
   439   let
   417     val all_visible =
   440     val all_visible =
   418       Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
   441       Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
   420     val required =
   443     val required =
   421       fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
   444       fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
   422         all_visible Symtab.empty;
   445         all_visible Symtab.empty;
   423   in Symtab.defined required end;
   446   in Symtab.defined required end;
   424 
   447 
       
   448 fun check_theory nodes name =
       
   449   is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
       
   450   is_some (Exn.get_res (get_header (get_node nodes name)));
       
   451 
   425 fun init_theory deps name node =
   452 fun init_theory deps name node =
   426   let
   453   let
   427     val (thy_name, imports, uses) = Exn.release (get_header node);
   454     val (thy_name, imports, uses) = Exn.release (get_header node);
   428     (* FIXME provide files via Scala layer *)
   455     (* FIXME provide files via Scala layer *)
   429     val (dir, files) =
   456     val (dir, files) =
   457           then Future.value (([], [], []), node)
   484           then Future.value (([], [], []), node)
   458           else
   485           else
   459             let
   486             let
   460               val node0 = node_of old_version name;
   487               val node0 = node_of old_version name;
   461               fun init () = init_theory deps name node;
   488               fun init () = init_theory deps name node;
       
   489               val bad_init =
       
   490                 not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   462             in
   491             in
   463               (singleton o Future.forks)
   492               (singleton o Future.forks)
   464                 {name = "Document.update", group = NONE,
   493                 {name = "Document.update", group = NONE,
   465                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   494                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
   466                 (fn () =>
   495                 (fn () =>
   467                   let
   496                   let
   468                     val required = is_required name;
   497                     val required = is_required name;
   469                     val last_visible = #2 (get_perspective node);
   498                     val last_visible = #2 (get_perspective node);
   470                     val (common, visible) = last_common last_visible node0 node;
   499                     val (common, (visible, initial)) = last_common state last_visible node0 node;
   471                     val common_exec = the_exec state (the_default_entry node common);
   500                     val common_exec = the_exec state (the_default_entry node common);
   472 
   501 
   473                     val (execs, exec) = ([], common_exec) |>
   502                     val (execs, exec, _) =
       
   503                       ([], common_exec, if initial then SOME init else NONE) |>
   474                       (visible orelse required) ?
   504                       (visible orelse required) ?
   475                         iterate_entries (after_entry node common)
   505                         iterate_entries_after common
   476                           (fn ((prev, id), _) => fn res =>
   506                           (fn ((prev, id), _) => fn res =>
   477                             if not required andalso prev = last_visible then NONE
   507                             if not required andalso prev = last_visible then NONE
   478                             else SOME (new_exec state init id res)) node;
   508                             else new_exec state bad_init id res) node;
   479 
   509 
   480                     val no_execs =
   510                     val no_execs =
   481                       iterate_entries (after_entry node0 common)
   511                       iterate_entries_after common
   482                         (fn ((_, id0), exec0) => fn res =>
   512                         (fn ((_, id0), exec0) => fn res =>
   483                           if is_none exec0 then NONE
   513                           if is_none exec0 then NONE
   484                           else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
   514                           else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
   485                           else SOME (id0 :: res)) node0 [];
   515                           else SOME (id0 :: res)) node0 [];
   486 
   516 
   536         nodes_of version |> Graph.schedule
   566         nodes_of version |> Graph.schedule
   537           (fn deps => fn (name, node) =>
   567           (fn deps => fn (name, node) =>
   538             (singleton o Future.forks)
   568             (singleton o Future.forks)
   539               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   569               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   540                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   570                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   541               (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   571               (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   542 
   572 
   543     in (versions, commands, execs, execution) end);
   573     in (versions, commands, execs, execution) end);
   544 
   574 
   545 
   575 
   546 
   576