--- a/etc/options Mon May 14 18:19:35 2018 +0200
+++ b/etc/options Mon May 14 22:23:25 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/General/position.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/General/position.ML Mon May 14 22:23:25 2018 +0200
@@ -14,8 +14,8 @@
val end_offset_of: T -> int option
val file_of: T -> string option
val advance: Symbol.symbol -> T -> T
- val advance_offset: int -> T -> T
- val distance_of: T -> T -> int
+ val advance_offsets: int -> T -> T
+ val distance_of: T * T -> int option
val none: T
val start: T
val file_name: string -> Properties.T
@@ -30,6 +30,7 @@
val get_id: T -> string option
val put_id: string -> T -> T
val parse_id: T -> int option
+ val adjust_offsets: (int -> int option) -> T -> T
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val offset_properties_of: T -> Properties.T
@@ -104,17 +105,17 @@
fun advance sym (pos as (Pos (count, props))) =
if invalid_count count then pos else Pos (advance_count sym count, props);
-fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
- if invalid_count count then pos
+fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
+ if offset = 0 orelse invalid_count count then pos
+ else if offset < 0 then raise Fail "Illegal offset"
else if valid i then raise Fail "Illegal line position"
- else Pos ((i, if_valid j (j + offset), k), props);
+ else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
(* distance of adjacent positions *)
-fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
- if valid j andalso valid j' then j' - j
- else 0;
+fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
+ if valid j andalso valid j' then SOME (j' - j) else NONE;
(* make position *)
@@ -144,6 +145,17 @@
fun parse_id pos = Option.map Value.parse_int (get_id pos);
+fun adjust_offsets adjust (pos as Pos (_, props)) =
+ (case parse_id pos of
+ SOME id =>
+ (case adjust id of
+ SOME offset =>
+ let val Pos (count, _) = advance_offsets offset pos
+ in Pos (count, Properties.remove Markup.idN props) end
+ | NONE => pos)
+ | NONE => pos);
+
+
(* markup properties *)
fun get props name =
--- a/src/Pure/General/symbol_pos.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/General/symbol_pos.ML Mon May 14 22:23:25 2018 +0200
@@ -244,7 +244,7 @@
| pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
let
val end_pos1 = Position.advance s1 pos1;
- val d = Int.max (0, Position.distance_of end_pos1 pos2);
+ val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
in s1 :: replicate d Symbol.DEL @ pad rest end;
val implode = implode o pad;
--- a/src/Pure/Isar/outer_syntax.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon May 14 22:23:25 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/Isar/token.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Isar/token.ML Mon May 14 22:23:25 2018 +0200
@@ -31,6 +31,7 @@
Files of file Exn.result list
val pos_of: T -> Position.T
val range_of: T list -> Position.range
+ val adjust_offsets: (int -> int option) -> T -> T
val eof: T
val is_eof: T -> bool
val not_eof: T -> bool
@@ -192,6 +193,9 @@
in Position.range (pos_of tok, pos') end
| range_of [] = Position.no_range;
+fun adjust_offsets adjust (Token ((x, range), y, z)) =
+ Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
+
(* stopper *)
@@ -681,7 +685,7 @@
fun make ((k, n), s) pos =
let
- val pos' = Position.advance_offset n pos;
+ val pos' = Position.advance_offsets n pos;
val range = Position.range (pos, pos');
val tok =
if 0 <= k andalso k < Vector.length immediate_kinds then
--- a/src/Pure/PIDE/command.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/PIDE/command.ML Mon May 14 22:23:25 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/command_span.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/PIDE/command_span.ML Mon May 14 22:23:25 2018 +0200
@@ -10,6 +10,9 @@
datatype span = Span of kind * Token.T list
val kind: span -> kind
val content: span -> Token.T list
+ val symbol_length: span -> int option
+ val adjust_offsets_kind: (int -> int option) -> kind -> kind
+ val adjust_offsets: (int -> int option) -> span -> span
end;
structure Command_Span: COMMAND_SPAN =
@@ -20,5 +23,14 @@
fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;
+val symbol_length = Position.distance_of o Token.range_of o content;
+
+fun adjust_offsets_kind adjust k =
+ (case k of
+ Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
+ | _ => k);
+
+fun adjust_offsets adjust (Span (k, toks)) =
+ Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
end;
--- a/src/Pure/PIDE/document.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/PIDE/document.ML Mon May 14 22:23:25 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/export_theory.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Mon May 14 22:23:25 2018 +0200
@@ -42,7 +42,7 @@
fun present_decls get_space get_decls =
present get_space get_decls o export_decls;
-val setup_presentation = Theory.setup o Thy_Info.add_presentation;
+fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (K f));
(* types *)
--- a/src/Pure/Thy/present.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Thy/present.ML Mon May 14 22:23:25 2018 +0200
@@ -8,12 +8,12 @@
sig
val get_bibtex_entries: theory -> string list
val theory_qualifier: theory -> string
- val document_enabled: string -> bool
+ val document_option: Options.T -> {enabled: bool, disabled: bool}
val document_variants: string -> (string * string) list
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
val finish: unit -> unit
- val theory_output: Position.T -> theory -> Latex.text list -> unit
+ val theory_output: theory -> string list -> unit
val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
end;
@@ -56,7 +56,7 @@
(* type theory_info *)
-type theory_info = {tex_source: string, html_source: string};
+type theory_info = {tex_source: string list, html_source: string};
fun make_theory_info (tex_source, html_source) =
{tex_source = tex_source, html_source = html_source}: theory_info;
@@ -142,7 +142,11 @@
(* options *)
-fun document_enabled s = s <> "" andalso s <> "false";
+fun document_option options =
+ (case Options.string options "document" of
+ "" => {enabled = false, disabled = false}
+ | "false" => {enabled = false, disabled = true}
+ | _ => {enabled = true, disabled = false});
fun document_variants str =
let
@@ -250,7 +254,7 @@
val _ = write_tex_index tex_index doc_dir;
val _ =
List.app (fn (a, {tex_source, ...}) =>
- write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
+ write_tex (fold Buffer.add tex_source Buffer.empty) a doc_dir) thys;
in
fn () =>
(isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
@@ -277,15 +281,10 @@
(* theory elements *)
-fun theory_output pos thy body =
+fun theory_output thy output =
with_session_info () (fn _ =>
if is_session_theory thy then
- let val name = Context.theory_name thy in
- (change_theory_info name o apfst)
- (fn _ =>
- let val latex = Latex.isabelle_body name body
- in Latex.output_text latex ^ Latex.output_positions pos latex end)
- end
+ (change_theory_info (Context.theory_name thy) o apfst) (K output)
else ());
fun theory_link (curr_chapter, curr_session) thy =
@@ -310,7 +309,7 @@
(Option.map Url.File (theory_link (chapter, session_name) parent),
(Context.theory_name parent)));
val html_source = HTML.theory symbols name parent_specs (mk_text ());
- val _ = init_theory_info name (make_theory_info ("", html_source));
+ val _ = init_theory_info name (make_theory_info ([], html_source));
val bibtex_entries' =
if is_session_theory thy then
--- a/src/Pure/Thy/thy_info.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon May 14 22:23:25 2018 +0200
@@ -7,20 +7,22 @@
signature THY_INFO =
sig
- val add_presentation: (theory -> unit) -> theory -> theory
- val apply_presentation: theory -> unit
+ type presentation_context =
+ {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
val lookup_theory: string -> theory option
val get_theory: string -> theory
val master_directory: string -> Path.T
val remove_thy: string -> unit
- val use_theories:
- {document: bool,
+ type context =
+ {options: Options.T,
symbols: HTML.symbols,
bibtex_entries: string list,
- last_timing: Toplevel.transition -> Time.time,
- qualifier: string,
- master_dir: Path.T} -> (string * Position.T) list -> unit
+ last_timing: Toplevel.transition -> Time.time}
+ val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
val use_thy: string -> unit
val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
@@ -32,18 +34,40 @@
(** presentation of consolidated theory **)
+type presentation_context =
+ {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
+ segments: Thy_Output.segment list};
+
structure Presentation = Theory_Data
(
- type T = ((theory -> unit) * stamp) list;
+ type T = ((presentation_context -> theory -> unit) * stamp) list;
val empty = [];
val extend = I;
fun merge data : T = Library.merge (eq_snd op =) data;
);
+fun apply_presentation (context: presentation_context) thy =
+ ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+
fun add_presentation f = Presentation.map (cons (f, stamp ()));
-fun apply_presentation thy =
- ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f thy));
+val _ =
+ Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+ if exists (Toplevel.is_skipped_proof o #state) segments then ()
+ else
+ let
+ val body = Thy_Output.present_thy thy segments;
+ val option = Present.document_option options;
+ in
+ if #disabled option then ()
+ else
+ let
+ val latex = Latex.isabelle_body (Context.theory_name thy) body;
+ 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
+ end));
@@ -155,6 +179,21 @@
fun update_thy deps theory = change_thys (update deps theory);
+(* context *)
+
+type context =
+ {options: Options.T,
+ symbols: HTML.symbols,
+ bibtex_entries: string list,
+ last_timing: Toplevel.transition -> Time.time};
+
+fun default_context (): context =
+ {options = Options.default (),
+ symbols = HTML.no_symbols,
+ bibtex_entries = [],
+ last_timing = K Time.zeroTime};
+
+
(* scheduling loader tasks *)
datatype result =
@@ -259,16 +298,15 @@
val thy = Toplevel.end_theory end_pos end_state;
in (results, thy) end;
-fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
- text_pos text parents =
+fun eval_thy (context: context) update_time master_dir header text_pos text parents =
let
+ val {options, symbols, bibtex_entries, last_timing} = context;
val (name, _) = #name header;
val keywords =
fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
(Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
- val toks = Token.explode keywords text_pos text;
- val spans = Outer_Syntax.parse_spans toks;
+ val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
val elements = Thy_Syntax.parse_elements keywords spans;
fun init () =
@@ -282,15 +320,11 @@
fun present () =
let
- val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
- val _ = apply_presentation thy;
- in
- if exists (Toplevel.is_skipped_proof o #2) res then ()
- else
- let val body = Thy_Output.present_thy thy res toks;
- in if document then Present.theory_output text_pos thy body else () end
- end;
-
+ val segments = (spans ~~ maps Toplevel.join_results results)
+ |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
+ 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;
@@ -402,20 +436,13 @@
(* use theories *)
-fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
- let
- val context =
- {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
- last_timing = last_timing};
- val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
+fun use_theories context qualifier master_dir imports =
+ let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
fun use_thy name =
- use_theories
- {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
- last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
- master_dir = Path.current}
- [(name, Position.none)];
+ use_theories (default_context ()) Resources.default_qualifier
+ Path.current [(name, Position.none)];
(* toplevel scripting -- without maintaining database *)
--- a/src/Pure/Thy/thy_output.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon May 14 22:23:25 2018 +0200
@@ -10,8 +10,8 @@
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
val output_token: Proof.context -> Token.T -> Latex.text list
val output_source: Proof.context -> string -> Latex.text list
- val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
- Token.T list -> Latex.text list
+ type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
+ val present_thy: theory -> segment list -> Latex.text list
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val lines: Latex.text list -> Latex.text list
@@ -338,7 +338,9 @@
in
-fun present_thy thy command_results toks =
+type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
+
+fun present_thy thy (segments: segment list) =
let
val keywords = Thy_Header.get_keywords thy;
@@ -404,13 +406,18 @@
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
- val spans = toks
+ val spans = segments
+ |> maps (Command_Span.content o #span)
|> drop_suffix Token.is_space
|> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
|> Source.source stopper (Scan.error (Scan.bulk span))
|> Source.exhaust;
+ val command_results =
+ segments |> map_filter (fn {command, state, ...} =>
+ if Toplevel.is_ignored command then NONE else SOME (command, state));
+
(* present commands *)
@@ -421,11 +428,11 @@
(present_span thy keywords document_tags span st st');
fun present _ [] = I
- | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
+ | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
in
if length command_results = length spans then
((NONE, []), NONE, true, [], (I, I))
- |> present Toplevel.toplevel (command_results ~~ spans)
+ |> present Toplevel.toplevel (spans ~~ command_results)
|> present_trailer
|> rev
else error "Messed-up outer syntax for presentation"
--- a/src/Pure/Tools/build.ML Mon May 14 18:19:35 2018 +0200
+++ b/src/Pure/Tools/build.ML Mon May 14 22:23:25 2018 +0200
@@ -113,6 +113,9 @@
fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
let
+ val context =
+ {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
+ last_timing = last_timing};
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
in
@@ -121,13 +124,7 @@
Options.set_default options;
Isabelle_Process.init_options ();
Future.fork I;
- (Thy_Info.use_theories {
- document = Present.document_enabled (Options.string options "document"),
- symbols = symbols,
- bibtex_entries = bibtex_entries,
- last_timing = last_timing,
- qualifier = qualifier,
- master_dir = master_dir}
+ (Thy_Info.use_theories context qualifier master_dir
|>
(case Options.string options "profiling" of
"" => I