support for dynamic document output while editing;
authorwenzelm
Mon May 14 22:22:47 2018 +0200 (16 months ago)
changeset 681846c693b2700b3
parent 68183 6560324b1e4d
child 68185 c80b0a35eb54
support for dynamic document output while editing;
etc/options
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/etc/options	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/etc/options	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -189,6 +189,9 @@
     1.4  option editor_syslog_limit : int = 100
     1.5    -- "maximum amount of buffered syslog messages"
     1.6  
     1.7 +public option editor_document_output : bool = false
     1.8 +  -- "dynamic document output while editing"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 14 22:01:00 2018 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 14 22:22:47 2018 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4    val parse_tokens: theory -> Token.T list -> Toplevel.transition list
     2.5    val parse: theory -> Position.T -> string -> Toplevel.transition list
     2.6    val parse_spans: Token.T list -> Command_Span.span list
     2.7 +  val make_span: Token.T list -> Command_Span.span
     2.8    val command_reports: theory -> Token.T -> Position.report_text list
     2.9    val check_command: Proof.context -> command_keyword -> string
    2.10  end;
    2.11 @@ -260,6 +261,11 @@
    2.12  
    2.13  end;
    2.14  
    2.15 +fun make_span toks =
    2.16 +  (case parse_spans toks of
    2.17 +    [span] => span
    2.18 +  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
    2.19 +
    2.20  
    2.21  (* check commands *)
    2.22  
     3.1 --- a/src/Pure/PIDE/command.ML	Mon May 14 22:01:00 2018 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Mon May 14 22:22:47 2018 +0200
     3.3 @@ -12,13 +12,15 @@
     3.4    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     3.5      blob list * int -> Token.T list -> Toplevel.transition
     3.6    type eval
     3.7 +  val eval_command_id: eval -> Document_ID.command
     3.8    val eval_exec_id: eval -> Document_ID.exec
     3.9    val eval_eq: eval * eval -> bool
    3.10    val eval_running: eval -> bool
    3.11    val eval_finished: eval -> bool
    3.12 +  val eval_result_command: eval -> Toplevel.transition
    3.13    val eval_result_state: eval -> Toplevel.state
    3.14    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    3.15 -    blob list * int -> Token.T list -> eval -> eval
    3.16 +    blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
    3.17    type print
    3.18    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    3.19      eval -> print list -> print list option
    3.20 @@ -161,7 +163,11 @@
    3.21    command = Toplevel.empty,
    3.22    state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
    3.23  
    3.24 -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    3.25 +datatype eval =
    3.26 +  Eval of
    3.27 +    {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy};
    3.28 +
    3.29 +fun eval_command_id (Eval {command_id, ...}) = command_id;
    3.30  
    3.31  fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    3.32  val eval_eq = op = o apply2 eval_exec_id;
    3.33 @@ -172,6 +178,7 @@
    3.34  fun eval_result (Eval {eval_process, ...}) =
    3.35    task_context (Future.worker_subgroup ()) Lazy.force eval_process;
    3.36  
    3.37 +val eval_result_command = #command o eval_result;
    3.38  val eval_result_state = #state o eval_result;
    3.39  
    3.40  local
    3.41 @@ -259,7 +266,7 @@
    3.42  
    3.43  in
    3.44  
    3.45 -fun eval keywords master_dir init blobs_info span eval0 =
    3.46 +fun eval keywords master_dir init blobs_info command_id span eval0 =
    3.47    let
    3.48      val exec_id = Document_ID.make ();
    3.49      fun process () =
    3.50 @@ -271,7 +278,9 @@
    3.51              (fn () =>
    3.52                read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
    3.53        in eval_state keywords span tr eval_state0 end;
    3.54 -  in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
    3.55 +  in
    3.56 +    Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process}
    3.57 +  end;
    3.58  
    3.59  end;
    3.60  
    3.61 @@ -404,7 +413,9 @@
    3.62  type exec = eval * print list;
    3.63  
    3.64  fun init_exec opt_thy : exec =
    3.65 -  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    3.66 +  (Eval
    3.67 +    {command_id = Document_ID.none, exec_id = Document_ID.none,
    3.68 +      eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    3.69  
    3.70  val no_exec = init_exec NONE;
    3.71  
    3.72 @@ -423,7 +434,7 @@
    3.73  fun ignore_process process =
    3.74    Lazy.is_running process orelse Lazy.is_finished process;
    3.75  
    3.76 -fun run_eval execution_id (Eval {exec_id, eval_process}) =
    3.77 +fun run_eval execution_id (Eval {exec_id, eval_process, ...}) =
    3.78    if Lazy.is_finished eval_process then ()
    3.79    else run_process execution_id exec_id eval_process;
    3.80  
     4.1 --- a/src/Pure/PIDE/document.ML	Mon May 14 22:01:00 2018 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Mon May 14 22:22:47 2018 +0200
     4.3 @@ -177,33 +177,16 @@
     4.4    | NONE => false);
     4.5  
     4.6  fun finished_result_theory node =
     4.7 -  finished_result node andalso
     4.8 +  if finished_result node then
     4.9      let val st = Command.eval_result_state (the (get_result node))
    4.10 -    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
    4.11 +    in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
    4.12 +  else NONE;
    4.13  
    4.14  val reset_consolidated =
    4.15    map_node (fn (header, keywords, perspective, entries, result, _) =>
    4.16      (header, keywords, perspective, entries, result, Lazy.lazy I));
    4.17  
    4.18 -fun check_consolidated (node as Node {consolidated, ...}) =
    4.19 -  Lazy.is_finished consolidated orelse
    4.20 -  finished_result_theory node andalso
    4.21 -    let
    4.22 -      val result_id = Command.eval_exec_id (the (get_result node));
    4.23 -      val eval_ids =
    4.24 -        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    4.25 -          (case opt_exec of
    4.26 -            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    4.27 -          | NONE => NONE)) node [];
    4.28 -    in
    4.29 -      (case Execution.snapshot eval_ids of
    4.30 -        [] =>
    4.31 -         (Lazy.force consolidated;
    4.32 -          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
    4.33 -            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
    4.34 -          true)
    4.35 -      | _ => false)
    4.36 -    end;
    4.37 +fun get_consolidated (Node {consolidated, ...}) = consolidated;
    4.38  
    4.39  fun get_node nodes name = String_Graph.get_node nodes name
    4.40    handle String_Graph.UNDEF _ => empty_node;
    4.41 @@ -428,6 +411,9 @@
    4.42  
    4.43  val the_command_name = #1 oo the_command;
    4.44  
    4.45 +fun force_command_span state =
    4.46 +  Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
    4.47 +
    4.48  
    4.49  (* execution *)
    4.50  
    4.51 @@ -527,8 +513,72 @@
    4.52      in (versions, blobs, commands, execution') end));
    4.53  
    4.54  fun consolidate_execution state =
    4.55 -  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
    4.56 -    (nodes_of (get_execution_version state)) ();
    4.57 +  let
    4.58 +    fun check_consolidated node_name node =
    4.59 +      if Lazy.is_finished (get_consolidated node) then ()
    4.60 +      else
    4.61 +        (case finished_result_theory node of
    4.62 +          NONE => ()
    4.63 +        | SOME thy =>
    4.64 +            let
    4.65 +              val result_id = Command.eval_exec_id (the (get_result node));
    4.66 +              val eval_ids =
    4.67 +                iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    4.68 +                  (case opt_exec of
    4.69 +                    SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    4.70 +                  | NONE => NONE)) node [];
    4.71 +            in
    4.72 +              (case Execution.snapshot eval_ids of
    4.73 +                [] =>
    4.74 +                  let
    4.75 +                    val (_, offsets, rev_segments) =
    4.76 +                      iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
    4.77 +                        (case opt_exec of
    4.78 +                          SOME (eval, _) =>
    4.79 +                            let
    4.80 +                              val command_id = Command.eval_command_id eval;
    4.81 +                              val span = force_command_span state command_id;
    4.82 +
    4.83 +                              val exec_id = Command.eval_exec_id eval;
    4.84 +                              val tr = Command.eval_result_command eval;
    4.85 +                              val st' = Command.eval_result_state eval;
    4.86 +
    4.87 +                              val offset' = offset + the_default 0 (Command_Span.symbol_length span);
    4.88 +                              val offsets' = offsets
    4.89 +                                |> Inttab.update (command_id, offset)
    4.90 +                                |> Inttab.update (exec_id, offset);
    4.91 +                              val segments' = (span, tr, st') :: segments;
    4.92 +                            in SOME (offset', offsets', segments') end
    4.93 +                        | NONE => NONE)) node (0, Inttab.empty, []);
    4.94 +
    4.95 +                    val adjust = Inttab.lookup offsets;
    4.96 +                    val adjust_pos = Position.adjust_offsets adjust;
    4.97 +                    val adjust_token = Token.adjust_offsets adjust;
    4.98 +                    val segments =
    4.99 +                      rev rev_segments |> map (fn (span, tr, st') =>
   4.100 +                        {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
   4.101 +
   4.102 +                    val presentation_context: Thy_Info.presentation_context =
   4.103 +                     {options = Options.default (),
   4.104 +                      file_pos = Position.file node_name,
   4.105 +                      adjust_pos = adjust_pos,
   4.106 +                      segments = segments};
   4.107 +
   4.108 +                    val _ = Lazy.force (get_consolidated node);
   4.109 +                    val _ =
   4.110 +                      Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   4.111 +                        (fn () =>
   4.112 +                          (if Options.default_bool "editor_document_output" then
   4.113 +                            Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *)
   4.114 +                           else ();
   4.115 +                           Output.status (Markup.markup_only Markup.consolidated))) ();
   4.116 +                  in () end
   4.117 +              | _ => ())
   4.118 +            end);
   4.119 +      in
   4.120 +        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node)
   4.121 +          (nodes_of (get_execution_version state)) ()
   4.122 +      end;
   4.123  
   4.124  
   4.125  
   4.126 @@ -657,7 +707,7 @@
   4.127  
   4.128        val eval' =
   4.129          Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
   4.130 -          (blobs, blobs_index) span (#1 (#2 command_exec));
   4.131 +          (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
   4.132        val prints' =
   4.133          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
   4.134        val exec' = (eval', prints');
     5.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 22:01:00 2018 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 22:22:47 2018 +0200
     5.3 @@ -8,7 +8,8 @@
     5.4  signature THY_INFO =
     5.5  sig
     5.6    type presentation_context =
     5.7 -    {options: Options.T, pos: Position.T, segments: Thy_Output.segment list}
     5.8 +    {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     5.9 +      segments: Thy_Output.segment list}
    5.10    val apply_presentation: presentation_context -> theory -> unit
    5.11    val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
    5.12    val get_names: unit -> string list
    5.13 @@ -34,7 +35,8 @@
    5.14  (** presentation of consolidated theory **)
    5.15  
    5.16  type presentation_context =
    5.17 -  {options: Options.T, pos: Position.T, segments: Thy_Output.segment list};
    5.18 +  {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
    5.19 +    segments: Thy_Output.segment list};
    5.20  
    5.21  structure Presentation = Theory_Data
    5.22  (
    5.23 @@ -50,7 +52,7 @@
    5.24  fun add_presentation f = Presentation.map (cons (f, stamp ()));
    5.25  
    5.26  val _ =
    5.27 -  Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
    5.28 +  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
    5.29      if exists (Toplevel.is_skipped_proof o #state) segments then ()
    5.30      else
    5.31        let
    5.32 @@ -61,7 +63,7 @@
    5.33          else
    5.34            let
    5.35              val latex = Latex.isabelle_body (Context.theory_name thy) body;
    5.36 -            val output = [Latex.output_text latex, Latex.output_positions pos latex];
    5.37 +            val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
    5.38              val _ = Export.export thy "document.tex" output;
    5.39              val _ = if #enabled option then Present.theory_output thy output else ();
    5.40            in () end
    5.41 @@ -320,7 +322,8 @@
    5.42        let
    5.43          val segments = (spans ~~ maps Toplevel.join_results results)
    5.44            |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
    5.45 -        val context = {options = options, pos = text_pos, segments = segments};
    5.46 +        val context: presentation_context =
    5.47 +          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
    5.48        in apply_presentation context thy end;
    5.49    in (thy, present, size text) end;
    5.50