src/Pure/PIDE/document.ML
changeset 68184 6c693b2700b3
parent 67500 dfde99d59f6e
child 68197 7857817403e4
     1.1 --- a/src/Pure/PIDE/document.ML	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -177,33 +177,16 @@
     1.4    | NONE => false);
     1.5  
     1.6  fun finished_result_theory node =
     1.7 -  finished_result node andalso
     1.8 +  if finished_result node then
     1.9      let val st = Command.eval_result_state (the (get_result node))
    1.10 -    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
    1.11 +    in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
    1.12 +  else NONE;
    1.13  
    1.14  val reset_consolidated =
    1.15    map_node (fn (header, keywords, perspective, entries, result, _) =>
    1.16      (header, keywords, perspective, entries, result, Lazy.lazy I));
    1.17  
    1.18 -fun check_consolidated (node as Node {consolidated, ...}) =
    1.19 -  Lazy.is_finished consolidated orelse
    1.20 -  finished_result_theory node andalso
    1.21 -    let
    1.22 -      val result_id = Command.eval_exec_id (the (get_result node));
    1.23 -      val eval_ids =
    1.24 -        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    1.25 -          (case opt_exec of
    1.26 -            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    1.27 -          | NONE => NONE)) node [];
    1.28 -    in
    1.29 -      (case Execution.snapshot eval_ids of
    1.30 -        [] =>
    1.31 -         (Lazy.force consolidated;
    1.32 -          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
    1.33 -            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
    1.34 -          true)
    1.35 -      | _ => false)
    1.36 -    end;
    1.37 +fun get_consolidated (Node {consolidated, ...}) = consolidated;
    1.38  
    1.39  fun get_node nodes name = String_Graph.get_node nodes name
    1.40    handle String_Graph.UNDEF _ => empty_node;
    1.41 @@ -428,6 +411,9 @@
    1.42  
    1.43  val the_command_name = #1 oo the_command;
    1.44  
    1.45 +fun force_command_span state =
    1.46 +  Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
    1.47 +
    1.48  
    1.49  (* execution *)
    1.50  
    1.51 @@ -527,8 +513,72 @@
    1.52      in (versions, blobs, commands, execution') end));
    1.53  
    1.54  fun consolidate_execution state =
    1.55 -  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
    1.56 -    (nodes_of (get_execution_version state)) ();
    1.57 +  let
    1.58 +    fun check_consolidated node_name node =
    1.59 +      if Lazy.is_finished (get_consolidated node) then ()
    1.60 +      else
    1.61 +        (case finished_result_theory node of
    1.62 +          NONE => ()
    1.63 +        | SOME thy =>
    1.64 +            let
    1.65 +              val result_id = Command.eval_exec_id (the (get_result node));
    1.66 +              val eval_ids =
    1.67 +                iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    1.68 +                  (case opt_exec of
    1.69 +                    SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    1.70 +                  | NONE => NONE)) node [];
    1.71 +            in
    1.72 +              (case Execution.snapshot eval_ids of
    1.73 +                [] =>
    1.74 +                  let
    1.75 +                    val (_, offsets, rev_segments) =
    1.76 +                      iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
    1.77 +                        (case opt_exec of
    1.78 +                          SOME (eval, _) =>
    1.79 +                            let
    1.80 +                              val command_id = Command.eval_command_id eval;
    1.81 +                              val span = force_command_span state command_id;
    1.82 +
    1.83 +                              val exec_id = Command.eval_exec_id eval;
    1.84 +                              val tr = Command.eval_result_command eval;
    1.85 +                              val st' = Command.eval_result_state eval;
    1.86 +
    1.87 +                              val offset' = offset + the_default 0 (Command_Span.symbol_length span);
    1.88 +                              val offsets' = offsets
    1.89 +                                |> Inttab.update (command_id, offset)
    1.90 +                                |> Inttab.update (exec_id, offset);
    1.91 +                              val segments' = (span, tr, st') :: segments;
    1.92 +                            in SOME (offset', offsets', segments') end
    1.93 +                        | NONE => NONE)) node (0, Inttab.empty, []);
    1.94 +
    1.95 +                    val adjust = Inttab.lookup offsets;
    1.96 +                    val adjust_pos = Position.adjust_offsets adjust;
    1.97 +                    val adjust_token = Token.adjust_offsets adjust;
    1.98 +                    val segments =
    1.99 +                      rev rev_segments |> map (fn (span, tr, st') =>
   1.100 +                        {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
   1.101 +
   1.102 +                    val presentation_context: Thy_Info.presentation_context =
   1.103 +                     {options = Options.default (),
   1.104 +                      file_pos = Position.file node_name,
   1.105 +                      adjust_pos = adjust_pos,
   1.106 +                      segments = segments};
   1.107 +
   1.108 +                    val _ = Lazy.force (get_consolidated node);
   1.109 +                    val _ =
   1.110 +                      Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   1.111 +                        (fn () =>
   1.112 +                          (if Options.default_bool "editor_document_output" then
   1.113 +                            Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *)
   1.114 +                           else ();
   1.115 +                           Output.status (Markup.markup_only Markup.consolidated))) ();
   1.116 +                  in () end
   1.117 +              | _ => ())
   1.118 +            end);
   1.119 +      in
   1.120 +        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node)
   1.121 +          (nodes_of (get_execution_version state)) ()
   1.122 +      end;
   1.123  
   1.124  
   1.125  
   1.126 @@ -657,7 +707,7 @@
   1.127  
   1.128        val eval' =
   1.129          Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
   1.130 -          (blobs, blobs_index) span (#1 (#2 command_exec));
   1.131 +          (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
   1.132        val prints' =
   1.133          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
   1.134        val exec' = (eval', prints');