# HG changeset patch # User wenzelm # Date 1526329405 -7200 # Node ID c80b0a35eb5421d223f04433f2075fa47160eeb8 # Parent 3e4af46a6f6aaa903aff33ae6ca83825d74cca2d# Parent 6c693b2700b3e29334fac13417414cf3daa01f76 merged diff -r 3e4af46a6f6a -r c80b0a35eb54 etc/options --- 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" diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/General/position.ML --- 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 = diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/General/symbol_pos.ML --- 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; diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Isar/outer_syntax.ML --- 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 *) diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Isar/token.ML --- 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 diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/PIDE/command.ML --- 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; diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/PIDE/command_span.ML --- 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; diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/PIDE/document.ML --- 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'); diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Thy/export_theory.ML --- 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 *) diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Thy/present.ML --- 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 diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Thy/thy_info.ML --- 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 *) diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Thy/thy_output.ML --- 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" diff -r 3e4af46a6f6a -r c80b0a35eb54 src/Pure/Tools/build.ML --- 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