# HG changeset patch # User wenzelm # Date 1526329367 -7200 # Node ID 6c693b2700b3e29334fac13417414cf3daa01f76 # Parent 6560324b1e4dc36b5323040262b57e8bda09e97c support for dynamic document output while editing; diff -r 6560324b1e4d -r 6c693b2700b3 etc/options --- a/etc/options Mon May 14 22:01:00 2018 +0200 +++ b/etc/options Mon May 14 22:22:47 2018 +0200 @@ -189,6 +189,9 @@ option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" +public option editor_document_output : bool = false + -- "dynamic document output while editing" + section "Miscellaneous Tools" diff -r 6560324b1e4d -r 6c693b2700b3 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon May 14 22:01:00 2018 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Mon May 14 22:22:47 2018 +0200 @@ -25,6 +25,7 @@ val parse_tokens: theory -> Token.T list -> Toplevel.transition list val parse: theory -> Position.T -> string -> Toplevel.transition list val parse_spans: Token.T list -> Command_Span.span list + val make_span: Token.T list -> Command_Span.span val command_reports: theory -> Token.T -> Position.report_text list val check_command: Proof.context -> command_keyword -> string end; @@ -260,6 +261,11 @@ end; +fun make_span toks = + (case parse_spans toks of + [span] => span + | _ => Command_Span.Span (Command_Span.Malformed_Span, toks)); + (* check commands *) diff -r 6560324b1e4d -r 6c693b2700b3 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Mon May 14 22:01:00 2018 +0200 +++ b/src/Pure/PIDE/command.ML Mon May 14 22:22:47 2018 +0200 @@ -12,13 +12,15 @@ val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob list * int -> Token.T list -> Toplevel.transition type eval + val eval_command_id: eval -> Document_ID.command val eval_exec_id: eval -> Document_ID.exec val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool + val eval_result_command: eval -> Toplevel.transition val eval_result_state: eval -> Toplevel.state val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> - blob list * int -> Token.T list -> eval -> eval + blob list * int -> Document_ID.command -> Token.T list -> eval -> eval type print val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option @@ -161,7 +163,11 @@ command = Toplevel.empty, state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)}; -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy}; +datatype eval = + Eval of + {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy}; + +fun eval_command_id (Eval {command_id, ...}) = command_id; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; val eval_eq = op = o apply2 eval_exec_id; @@ -172,6 +178,7 @@ fun eval_result (Eval {eval_process, ...}) = task_context (Future.worker_subgroup ()) Lazy.force eval_process; +val eval_result_command = #command o eval_result; val eval_result_state = #state o eval_result; local @@ -259,7 +266,7 @@ in -fun eval keywords master_dir init blobs_info span eval0 = +fun eval keywords master_dir init blobs_info command_id span eval0 = let val exec_id = Document_ID.make (); fun process () = @@ -271,7 +278,9 @@ (fn () => read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); in eval_state keywords span tr eval_state0 end; - in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end; + in + Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} + end; end; @@ -404,7 +413,9 @@ type exec = eval * print list; fun init_exec opt_thy : exec = - (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []); + (Eval + {command_id = Document_ID.none, exec_id = Document_ID.none, + eval_process = Lazy.value (init_eval_state opt_thy)}, []); val no_exec = init_exec NONE; @@ -423,7 +434,7 @@ fun ignore_process process = Lazy.is_running process orelse Lazy.is_finished process; -fun run_eval execution_id (Eval {exec_id, eval_process}) = +fun run_eval execution_id (Eval {exec_id, eval_process, ...}) = if Lazy.is_finished eval_process then () else run_process execution_id exec_id eval_process; diff -r 6560324b1e4d -r 6c693b2700b3 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon May 14 22:01:00 2018 +0200 +++ b/src/Pure/PIDE/document.ML Mon May 14 22:22:47 2018 +0200 @@ -177,33 +177,16 @@ | NONE => false); fun finished_result_theory node = - finished_result node andalso + if finished_result node then let val st = Command.eval_result_state (the (get_result node)) - in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end; + in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end + else NONE; val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => (header, keywords, perspective, entries, result, Lazy.lazy I)); -fun check_consolidated (node as Node {consolidated, ...}) = - Lazy.is_finished consolidated orelse - finished_result_theory node andalso - let - val result_id = Command.eval_exec_id (the (get_result node)); - val eval_ids = - iterate_entries (fn (_, opt_exec) => fn eval_ids => - (case opt_exec of - SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) - | NONE => NONE)) node []; - in - (case Execution.snapshot eval_ids of - [] => - (Lazy.force consolidated; - Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) - (fn () => Output.status (Markup.markup_only Markup.consolidated)) (); - true) - | _ => false) - end; +fun get_consolidated (Node {consolidated, ...}) = consolidated; fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; @@ -428,6 +411,9 @@ val the_command_name = #1 oo the_command; +fun force_command_span state = + Outer_Syntax.make_span o Lazy.force o #4 o the_command state; + (* execution *) @@ -527,8 +513,72 @@ in (versions, blobs, commands, execution') end)); fun consolidate_execution state = - String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node)) - (nodes_of (get_execution_version state)) (); + let + fun check_consolidated node_name node = + if Lazy.is_finished (get_consolidated node) then () + else + (case finished_result_theory node of + NONE => () + | SOME thy => + let + val result_id = Command.eval_exec_id (the (get_result node)); + val eval_ids = + iterate_entries (fn (_, opt_exec) => fn eval_ids => + (case opt_exec of + SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) + | NONE => NONE)) node []; + in + (case Execution.snapshot eval_ids of + [] => + let + val (_, offsets, rev_segments) = + iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => + (case opt_exec of + SOME (eval, _) => + let + val command_id = Command.eval_command_id eval; + val span = force_command_span state command_id; + + val exec_id = Command.eval_exec_id eval; + val tr = Command.eval_result_command eval; + val st' = Command.eval_result_state eval; + + val offset' = offset + the_default 0 (Command_Span.symbol_length span); + val offsets' = offsets + |> Inttab.update (command_id, offset) + |> Inttab.update (exec_id, offset); + val segments' = (span, tr, st') :: segments; + in SOME (offset', offsets', segments') end + | NONE => NONE)) node (0, Inttab.empty, []); + + val adjust = Inttab.lookup offsets; + val adjust_pos = Position.adjust_offsets adjust; + val adjust_token = Token.adjust_offsets adjust; + val segments = + rev rev_segments |> map (fn (span, tr, st') => + {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); + + val presentation_context: Thy_Info.presentation_context = + {options = Options.default (), + file_pos = Position.file node_name, + adjust_pos = adjust_pos, + segments = segments}; + + val _ = Lazy.force (get_consolidated node); + val _ = + Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) + (fn () => + (if Options.default_bool "editor_document_output" then + Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *) + else (); + Output.status (Markup.markup_only Markup.consolidated))) (); + in () end + | _ => ()) + end); + in + String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node) + (nodes_of (get_execution_version state)) () + end; @@ -657,7 +707,7 @@ val eval' = Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) - (blobs, blobs_index) span (#1 (#2 command_exec)); + (blobs, blobs_index) command_id' span (#1 (#2 command_exec)); val prints' = perhaps (Command.print command_visible command_overlays keywords command_name eval') []; val exec' = (eval', prints'); diff -r 6560324b1e4d -r 6c693b2700b3 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon May 14 22:01:00 2018 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon May 14 22:22:47 2018 +0200 @@ -8,7 +8,8 @@ signature THY_INFO = sig type presentation_context = - {options: Options.T, pos: Position.T, segments: Thy_Output.segment list} + {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, + segments: Thy_Output.segment list} val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list @@ -34,7 +35,8 @@ (** presentation of consolidated theory **) type presentation_context = - {options: Options.T, pos: Position.T, segments: Thy_Output.segment list}; + {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, + segments: Thy_Output.segment list}; structure Presentation = Theory_Data ( @@ -50,7 +52,7 @@ fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = - Theory.setup (add_presentation (fn {options, pos, segments} => fn thy => + Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let @@ -61,7 +63,7 @@ else let val latex = Latex.isabelle_body (Context.theory_name thy) body; - val output = [Latex.output_text latex, Latex.output_positions pos latex]; + val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; val _ = Export.export thy "document.tex" output; val _ = if #enabled option then Present.theory_output thy output else (); in () end @@ -320,7 +322,8 @@ let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); - val context = {options = options, pos = text_pos, segments = segments}; + val context: presentation_context = + {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end;