--- 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"
--- 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 *)
--- 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;
--- 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');
--- 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;