merged
authorwenzelm
Mon May 14 22:23:25 2018 +0200 (12 months ago)
changeset 68185c80b0a35eb54
parent 68176 3e4af46a6f6a
parent 68184 6c693b2700b3
child 68187 48262e3a2bde
merged
     1.1 --- a/etc/options	Mon May 14 18:19:35 2018 +0200
     1.2 +++ b/etc/options	Mon May 14 22:23:25 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/General/position.ML	Mon May 14 18:19:35 2018 +0200
     2.2 +++ b/src/Pure/General/position.ML	Mon May 14 22:23:25 2018 +0200
     2.3 @@ -14,8 +14,8 @@
     2.4    val end_offset_of: T -> int option
     2.5    val file_of: T -> string option
     2.6    val advance: Symbol.symbol -> T -> T
     2.7 -  val advance_offset: int -> T -> T
     2.8 -  val distance_of: T -> T -> int
     2.9 +  val advance_offsets: int -> T -> T
    2.10 +  val distance_of: T * T -> int option
    2.11    val none: T
    2.12    val start: T
    2.13    val file_name: string -> Properties.T
    2.14 @@ -30,6 +30,7 @@
    2.15    val get_id: T -> string option
    2.16    val put_id: string -> T -> T
    2.17    val parse_id: T -> int option
    2.18 +  val adjust_offsets: (int -> int option) -> T -> T
    2.19    val of_properties: Properties.T -> T
    2.20    val properties_of: T -> Properties.T
    2.21    val offset_properties_of: T -> Properties.T
    2.22 @@ -104,17 +105,17 @@
    2.23  fun advance sym (pos as (Pos (count, props))) =
    2.24    if invalid_count count then pos else Pos (advance_count sym count, props);
    2.25  
    2.26 -fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
    2.27 -  if invalid_count count then pos
    2.28 +fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
    2.29 +  if offset = 0 orelse invalid_count count then pos
    2.30 +  else if offset < 0 then raise Fail "Illegal offset"
    2.31    else if valid i then raise Fail "Illegal line position"
    2.32 -  else Pos ((i, if_valid j (j + offset), k), props);
    2.33 +  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
    2.34  
    2.35  
    2.36  (* distance of adjacent positions *)
    2.37  
    2.38 -fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
    2.39 -  if valid j andalso valid j' then j' - j
    2.40 -  else 0;
    2.41 +fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
    2.42 +  if valid j andalso valid j' then SOME (j' - j) else NONE;
    2.43  
    2.44  
    2.45  (* make position *)
    2.46 @@ -144,6 +145,17 @@
    2.47  fun parse_id pos = Option.map Value.parse_int (get_id pos);
    2.48  
    2.49  
    2.50 +fun adjust_offsets adjust (pos as Pos (_, props)) =
    2.51 +  (case parse_id pos of
    2.52 +    SOME id =>
    2.53 +      (case adjust id of
    2.54 +        SOME offset =>
    2.55 +          let val Pos (count, _) = advance_offsets offset pos
    2.56 +          in Pos (count, Properties.remove Markup.idN props) end
    2.57 +      | NONE => pos)
    2.58 +  | NONE => pos);
    2.59 +
    2.60 +
    2.61  (* markup properties *)
    2.62  
    2.63  fun get props name =
     3.1 --- a/src/Pure/General/symbol_pos.ML	Mon May 14 18:19:35 2018 +0200
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Mon May 14 22:23:25 2018 +0200
     3.3 @@ -244,7 +244,7 @@
     3.4    | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
     3.5        let
     3.6          val end_pos1 = Position.advance s1 pos1;
     3.7 -        val d = Int.max (0, Position.distance_of end_pos1 pos2);
     3.8 +        val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
     3.9        in s1 :: replicate d Symbol.DEL @ pad rest end;
    3.10  
    3.11  val implode = implode o pad;
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 14 18:19:35 2018 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 14 22:23:25 2018 +0200
     4.3 @@ -25,6 +25,7 @@
     4.4    val parse_tokens: theory -> Token.T list -> Toplevel.transition list
     4.5    val parse: theory -> Position.T -> string -> Toplevel.transition list
     4.6    val parse_spans: Token.T list -> Command_Span.span list
     4.7 +  val make_span: Token.T list -> Command_Span.span
     4.8    val command_reports: theory -> Token.T -> Position.report_text list
     4.9    val check_command: Proof.context -> command_keyword -> string
    4.10  end;
    4.11 @@ -260,6 +261,11 @@
    4.12  
    4.13  end;
    4.14  
    4.15 +fun make_span toks =
    4.16 +  (case parse_spans toks of
    4.17 +    [span] => span
    4.18 +  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
    4.19 +
    4.20  
    4.21  (* check commands *)
    4.22  
     5.1 --- a/src/Pure/Isar/token.ML	Mon May 14 18:19:35 2018 +0200
     5.2 +++ b/src/Pure/Isar/token.ML	Mon May 14 22:23:25 2018 +0200
     5.3 @@ -31,6 +31,7 @@
     5.4      Files of file Exn.result list
     5.5    val pos_of: T -> Position.T
     5.6    val range_of: T list -> Position.range
     5.7 +  val adjust_offsets: (int -> int option) -> T -> T
     5.8    val eof: T
     5.9    val is_eof: T -> bool
    5.10    val not_eof: T -> bool
    5.11 @@ -192,6 +193,9 @@
    5.12        in Position.range (pos_of tok, pos') end
    5.13    | range_of [] = Position.no_range;
    5.14  
    5.15 +fun adjust_offsets adjust (Token ((x, range), y, z)) =
    5.16 +  Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
    5.17 +
    5.18  
    5.19  (* stopper *)
    5.20  
    5.21 @@ -681,7 +685,7 @@
    5.22  
    5.23  fun make ((k, n), s) pos =
    5.24    let
    5.25 -    val pos' = Position.advance_offset n pos;
    5.26 +    val pos' = Position.advance_offsets n pos;
    5.27      val range = Position.range (pos, pos');
    5.28      val tok =
    5.29        if 0 <= k andalso k < Vector.length immediate_kinds then
     6.1 --- a/src/Pure/PIDE/command.ML	Mon May 14 18:19:35 2018 +0200
     6.2 +++ b/src/Pure/PIDE/command.ML	Mon May 14 22:23:25 2018 +0200
     6.3 @@ -12,13 +12,15 @@
     6.4    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     6.5      blob list * int -> Token.T list -> Toplevel.transition
     6.6    type eval
     6.7 +  val eval_command_id: eval -> Document_ID.command
     6.8    val eval_exec_id: eval -> Document_ID.exec
     6.9    val eval_eq: eval * eval -> bool
    6.10    val eval_running: eval -> bool
    6.11    val eval_finished: eval -> bool
    6.12 +  val eval_result_command: eval -> Toplevel.transition
    6.13    val eval_result_state: eval -> Toplevel.state
    6.14    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    6.15 -    blob list * int -> Token.T list -> eval -> eval
    6.16 +    blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
    6.17    type print
    6.18    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    6.19      eval -> print list -> print list option
    6.20 @@ -161,7 +163,11 @@
    6.21    command = Toplevel.empty,
    6.22    state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
    6.23  
    6.24 -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    6.25 +datatype eval =
    6.26 +  Eval of
    6.27 +    {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy};
    6.28 +
    6.29 +fun eval_command_id (Eval {command_id, ...}) = command_id;
    6.30  
    6.31  fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    6.32  val eval_eq = op = o apply2 eval_exec_id;
    6.33 @@ -172,6 +178,7 @@
    6.34  fun eval_result (Eval {eval_process, ...}) =
    6.35    task_context (Future.worker_subgroup ()) Lazy.force eval_process;
    6.36  
    6.37 +val eval_result_command = #command o eval_result;
    6.38  val eval_result_state = #state o eval_result;
    6.39  
    6.40  local
    6.41 @@ -259,7 +266,7 @@
    6.42  
    6.43  in
    6.44  
    6.45 -fun eval keywords master_dir init blobs_info span eval0 =
    6.46 +fun eval keywords master_dir init blobs_info command_id span eval0 =
    6.47    let
    6.48      val exec_id = Document_ID.make ();
    6.49      fun process () =
    6.50 @@ -271,7 +278,9 @@
    6.51              (fn () =>
    6.52                read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
    6.53        in eval_state keywords span tr eval_state0 end;
    6.54 -  in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
    6.55 +  in
    6.56 +    Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process}
    6.57 +  end;
    6.58  
    6.59  end;
    6.60  
    6.61 @@ -404,7 +413,9 @@
    6.62  type exec = eval * print list;
    6.63  
    6.64  fun init_exec opt_thy : exec =
    6.65 -  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    6.66 +  (Eval
    6.67 +    {command_id = Document_ID.none, exec_id = Document_ID.none,
    6.68 +      eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    6.69  
    6.70  val no_exec = init_exec NONE;
    6.71  
    6.72 @@ -423,7 +434,7 @@
    6.73  fun ignore_process process =
    6.74    Lazy.is_running process orelse Lazy.is_finished process;
    6.75  
    6.76 -fun run_eval execution_id (Eval {exec_id, eval_process}) =
    6.77 +fun run_eval execution_id (Eval {exec_id, eval_process, ...}) =
    6.78    if Lazy.is_finished eval_process then ()
    6.79    else run_process execution_id exec_id eval_process;
    6.80  
     7.1 --- a/src/Pure/PIDE/command_span.ML	Mon May 14 18:19:35 2018 +0200
     7.2 +++ b/src/Pure/PIDE/command_span.ML	Mon May 14 22:23:25 2018 +0200
     7.3 @@ -10,6 +10,9 @@
     7.4    datatype span = Span of kind * Token.T list
     7.5    val kind: span -> kind
     7.6    val content: span -> Token.T list
     7.7 +  val symbol_length: span -> int option
     7.8 +  val adjust_offsets_kind: (int -> int option) -> kind -> kind
     7.9 +  val adjust_offsets: (int -> int option) -> span -> span
    7.10  end;
    7.11  
    7.12  structure Command_Span: COMMAND_SPAN =
    7.13 @@ -20,5 +23,14 @@
    7.14  
    7.15  fun kind (Span (k, _)) = k;
    7.16  fun content (Span (_, toks)) = toks;
    7.17 +val symbol_length = Position.distance_of o Token.range_of o content;
    7.18 +
    7.19 +fun adjust_offsets_kind adjust k =
    7.20 +  (case k of
    7.21 +    Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
    7.22 +  | _ => k);
    7.23 +
    7.24 +fun adjust_offsets adjust (Span (k, toks)) =
    7.25 +  Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
    7.26  
    7.27  end;
     8.1 --- a/src/Pure/PIDE/document.ML	Mon May 14 18:19:35 2018 +0200
     8.2 +++ b/src/Pure/PIDE/document.ML	Mon May 14 22:23:25 2018 +0200
     8.3 @@ -177,33 +177,16 @@
     8.4    | NONE => false);
     8.5  
     8.6  fun finished_result_theory node =
     8.7 -  finished_result node andalso
     8.8 +  if finished_result node then
     8.9      let val st = Command.eval_result_state (the (get_result node))
    8.10 -    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
    8.11 +    in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
    8.12 +  else NONE;
    8.13  
    8.14  val reset_consolidated =
    8.15    map_node (fn (header, keywords, perspective, entries, result, _) =>
    8.16      (header, keywords, perspective, entries, result, Lazy.lazy I));
    8.17  
    8.18 -fun check_consolidated (node as Node {consolidated, ...}) =
    8.19 -  Lazy.is_finished consolidated orelse
    8.20 -  finished_result_theory node andalso
    8.21 -    let
    8.22 -      val result_id = Command.eval_exec_id (the (get_result node));
    8.23 -      val eval_ids =
    8.24 -        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    8.25 -          (case opt_exec of
    8.26 -            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    8.27 -          | NONE => NONE)) node [];
    8.28 -    in
    8.29 -      (case Execution.snapshot eval_ids of
    8.30 -        [] =>
    8.31 -         (Lazy.force consolidated;
    8.32 -          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
    8.33 -            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
    8.34 -          true)
    8.35 -      | _ => false)
    8.36 -    end;
    8.37 +fun get_consolidated (Node {consolidated, ...}) = consolidated;
    8.38  
    8.39  fun get_node nodes name = String_Graph.get_node nodes name
    8.40    handle String_Graph.UNDEF _ => empty_node;
    8.41 @@ -428,6 +411,9 @@
    8.42  
    8.43  val the_command_name = #1 oo the_command;
    8.44  
    8.45 +fun force_command_span state =
    8.46 +  Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
    8.47 +
    8.48  
    8.49  (* execution *)
    8.50  
    8.51 @@ -527,8 +513,72 @@
    8.52      in (versions, blobs, commands, execution') end));
    8.53  
    8.54  fun consolidate_execution state =
    8.55 -  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
    8.56 -    (nodes_of (get_execution_version state)) ();
    8.57 +  let
    8.58 +    fun check_consolidated node_name node =
    8.59 +      if Lazy.is_finished (get_consolidated node) then ()
    8.60 +      else
    8.61 +        (case finished_result_theory node of
    8.62 +          NONE => ()
    8.63 +        | SOME thy =>
    8.64 +            let
    8.65 +              val result_id = Command.eval_exec_id (the (get_result node));
    8.66 +              val eval_ids =
    8.67 +                iterate_entries (fn (_, opt_exec) => fn eval_ids =>
    8.68 +                  (case opt_exec of
    8.69 +                    SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
    8.70 +                  | NONE => NONE)) node [];
    8.71 +            in
    8.72 +              (case Execution.snapshot eval_ids of
    8.73 +                [] =>
    8.74 +                  let
    8.75 +                    val (_, offsets, rev_segments) =
    8.76 +                      iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
    8.77 +                        (case opt_exec of
    8.78 +                          SOME (eval, _) =>
    8.79 +                            let
    8.80 +                              val command_id = Command.eval_command_id eval;
    8.81 +                              val span = force_command_span state command_id;
    8.82 +
    8.83 +                              val exec_id = Command.eval_exec_id eval;
    8.84 +                              val tr = Command.eval_result_command eval;
    8.85 +                              val st' = Command.eval_result_state eval;
    8.86 +
    8.87 +                              val offset' = offset + the_default 0 (Command_Span.symbol_length span);
    8.88 +                              val offsets' = offsets
    8.89 +                                |> Inttab.update (command_id, offset)
    8.90 +                                |> Inttab.update (exec_id, offset);
    8.91 +                              val segments' = (span, tr, st') :: segments;
    8.92 +                            in SOME (offset', offsets', segments') end
    8.93 +                        | NONE => NONE)) node (0, Inttab.empty, []);
    8.94 +
    8.95 +                    val adjust = Inttab.lookup offsets;
    8.96 +                    val adjust_pos = Position.adjust_offsets adjust;
    8.97 +                    val adjust_token = Token.adjust_offsets adjust;
    8.98 +                    val segments =
    8.99 +                      rev rev_segments |> map (fn (span, tr, st') =>
   8.100 +                        {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
   8.101 +
   8.102 +                    val presentation_context: Thy_Info.presentation_context =
   8.103 +                     {options = Options.default (),
   8.104 +                      file_pos = Position.file node_name,
   8.105 +                      adjust_pos = adjust_pos,
   8.106 +                      segments = segments};
   8.107 +
   8.108 +                    val _ = Lazy.force (get_consolidated node);
   8.109 +                    val _ =
   8.110 +                      Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   8.111 +                        (fn () =>
   8.112 +                          (if Options.default_bool "editor_document_output" then
   8.113 +                            Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *)
   8.114 +                           else ();
   8.115 +                           Output.status (Markup.markup_only Markup.consolidated))) ();
   8.116 +                  in () end
   8.117 +              | _ => ())
   8.118 +            end);
   8.119 +      in
   8.120 +        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node)
   8.121 +          (nodes_of (get_execution_version state)) ()
   8.122 +      end;
   8.123  
   8.124  
   8.125  
   8.126 @@ -657,7 +707,7 @@
   8.127  
   8.128        val eval' =
   8.129          Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
   8.130 -          (blobs, blobs_index) span (#1 (#2 command_exec));
   8.131 +          (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
   8.132        val prints' =
   8.133          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
   8.134        val exec' = (eval', prints');
     9.1 --- a/src/Pure/Thy/export_theory.ML	Mon May 14 18:19:35 2018 +0200
     9.2 +++ b/src/Pure/Thy/export_theory.ML	Mon May 14 22:23:25 2018 +0200
     9.3 @@ -42,7 +42,7 @@
     9.4  fun present_decls get_space get_decls =
     9.5    present get_space get_decls o export_decls;
     9.6  
     9.7 -val setup_presentation = Theory.setup o Thy_Info.add_presentation;
     9.8 +fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (K f));
     9.9  
    9.10  
    9.11  (* types *)
    10.1 --- a/src/Pure/Thy/present.ML	Mon May 14 18:19:35 2018 +0200
    10.2 +++ b/src/Pure/Thy/present.ML	Mon May 14 22:23:25 2018 +0200
    10.3 @@ -8,12 +8,12 @@
    10.4  sig
    10.5    val get_bibtex_entries: theory -> string list
    10.6    val theory_qualifier: theory -> string
    10.7 -  val document_enabled: string -> bool
    10.8 +  val document_option: Options.T -> {enabled: bool, disabled: bool}
    10.9    val document_variants: string -> (string * string) list
   10.10    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
   10.11      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
   10.12    val finish: unit -> unit
   10.13 -  val theory_output: Position.T -> theory -> Latex.text list -> unit
   10.14 +  val theory_output: theory -> string list -> unit
   10.15    val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
   10.16  end;
   10.17  
   10.18 @@ -56,7 +56,7 @@
   10.19  
   10.20  (* type theory_info *)
   10.21  
   10.22 -type theory_info = {tex_source: string, html_source: string};
   10.23 +type theory_info = {tex_source: string list, html_source: string};
   10.24  
   10.25  fun make_theory_info (tex_source, html_source) =
   10.26    {tex_source = tex_source, html_source = html_source}: theory_info;
   10.27 @@ -142,7 +142,11 @@
   10.28  
   10.29  (* options *)
   10.30  
   10.31 -fun document_enabled s = s <> "" andalso s <> "false";
   10.32 +fun document_option options =
   10.33 +  (case Options.string options "document" of
   10.34 +    "" => {enabled = false, disabled = false}
   10.35 +  | "false" => {enabled = false, disabled = true}
   10.36 +  | _ => {enabled = true, disabled = false});
   10.37  
   10.38  fun document_variants str =
   10.39    let
   10.40 @@ -250,7 +254,7 @@
   10.41          val _ = write_tex_index tex_index doc_dir;
   10.42          val _ =
   10.43            List.app (fn (a, {tex_source, ...}) =>
   10.44 -            write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
   10.45 +            write_tex (fold Buffer.add tex_source Buffer.empty) a doc_dir) thys;
   10.46        in
   10.47          fn () =>
   10.48            (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
   10.49 @@ -277,15 +281,10 @@
   10.50  
   10.51  (* theory elements *)
   10.52  
   10.53 -fun theory_output pos thy body =
   10.54 +fun theory_output thy output =
   10.55    with_session_info () (fn _ =>
   10.56      if is_session_theory thy then
   10.57 -      let val name = Context.theory_name thy in
   10.58 -        (change_theory_info name o apfst)
   10.59 -          (fn _ =>
   10.60 -            let val latex = Latex.isabelle_body name body
   10.61 -            in Latex.output_text latex ^ Latex.output_positions pos latex end)
   10.62 -      end
   10.63 +      (change_theory_info (Context.theory_name thy) o apfst) (K output)
   10.64      else ());
   10.65  
   10.66  fun theory_link (curr_chapter, curr_session) thy =
   10.67 @@ -310,7 +309,7 @@
   10.68            (Option.map Url.File (theory_link (chapter, session_name) parent),
   10.69              (Context.theory_name parent)));
   10.70        val html_source = HTML.theory symbols name parent_specs (mk_text ());
   10.71 -      val _ = init_theory_info name (make_theory_info ("", html_source));
   10.72 +      val _ = init_theory_info name (make_theory_info ([], html_source));
   10.73  
   10.74        val bibtex_entries' =
   10.75          if is_session_theory thy then
    11.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 18:19:35 2018 +0200
    11.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 22:23:25 2018 +0200
    11.3 @@ -7,20 +7,22 @@
    11.4  
    11.5  signature THY_INFO =
    11.6  sig
    11.7 -  val add_presentation: (theory -> unit) -> theory -> theory
    11.8 -  val apply_presentation: theory -> unit
    11.9 +  type presentation_context =
   11.10 +    {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
   11.11 +      segments: Thy_Output.segment list}
   11.12 +  val apply_presentation: presentation_context -> theory -> unit
   11.13 +  val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   11.14    val get_names: unit -> string list
   11.15    val lookup_theory: string -> theory option
   11.16    val get_theory: string -> theory
   11.17    val master_directory: string -> Path.T
   11.18    val remove_thy: string -> unit
   11.19 -  val use_theories:
   11.20 -    {document: bool,
   11.21 +  type context =
   11.22 +    {options: Options.T,
   11.23       symbols: HTML.symbols,
   11.24       bibtex_entries: string list,
   11.25 -     last_timing: Toplevel.transition -> Time.time,
   11.26 -     qualifier: string,
   11.27 -     master_dir: Path.T} -> (string * Position.T) list -> unit
   11.28 +     last_timing: Toplevel.transition -> Time.time}
   11.29 +  val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
   11.30    val use_thy: string -> unit
   11.31    val script_thy: Position.T -> string -> theory -> theory
   11.32    val register_thy: theory -> unit
   11.33 @@ -32,18 +34,40 @@
   11.34  
   11.35  (** presentation of consolidated theory **)
   11.36  
   11.37 +type presentation_context =
   11.38 +  {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
   11.39 +    segments: Thy_Output.segment list};
   11.40 +
   11.41  structure Presentation = Theory_Data
   11.42  (
   11.43 -  type T = ((theory -> unit) * stamp) list;
   11.44 +  type T = ((presentation_context -> theory -> unit) * stamp) list;
   11.45    val empty = [];
   11.46    val extend = I;
   11.47    fun merge data : T = Library.merge (eq_snd op =) data;
   11.48  );
   11.49  
   11.50 +fun apply_presentation (context: presentation_context) thy =
   11.51 +  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
   11.52 +
   11.53  fun add_presentation f = Presentation.map (cons (f, stamp ()));
   11.54  
   11.55 -fun apply_presentation thy =
   11.56 -  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f thy));
   11.57 +val _ =
   11.58 +  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
   11.59 +    if exists (Toplevel.is_skipped_proof o #state) segments then ()
   11.60 +    else
   11.61 +      let
   11.62 +        val body = Thy_Output.present_thy thy segments;
   11.63 +        val option = Present.document_option options;
   11.64 +      in
   11.65 +        if #disabled option then ()
   11.66 +        else
   11.67 +          let
   11.68 +            val latex = Latex.isabelle_body (Context.theory_name thy) body;
   11.69 +            val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
   11.70 +            val _ = Export.export thy "document.tex" output;
   11.71 +            val _ = if #enabled option then Present.theory_output thy output else ();
   11.72 +          in () end
   11.73 +      end));
   11.74  
   11.75  
   11.76  
   11.77 @@ -155,6 +179,21 @@
   11.78  fun update_thy deps theory = change_thys (update deps theory);
   11.79  
   11.80  
   11.81 +(* context *)
   11.82 +
   11.83 +type context =
   11.84 +  {options: Options.T,
   11.85 +   symbols: HTML.symbols,
   11.86 +   bibtex_entries: string list,
   11.87 +   last_timing: Toplevel.transition -> Time.time};
   11.88 +
   11.89 +fun default_context (): context =
   11.90 +  {options = Options.default (),
   11.91 +   symbols = HTML.no_symbols,
   11.92 +   bibtex_entries = [],
   11.93 +   last_timing = K Time.zeroTime};
   11.94 +
   11.95 +
   11.96  (* scheduling loader tasks *)
   11.97  
   11.98  datatype result =
   11.99 @@ -259,16 +298,15 @@
  11.100      val thy = Toplevel.end_theory end_pos end_state;
  11.101    in (results, thy) end;
  11.102  
  11.103 -fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
  11.104 -    text_pos text parents =
  11.105 +fun eval_thy (context: context) update_time master_dir header text_pos text parents =
  11.106    let
  11.107 +    val {options, symbols, bibtex_entries, last_timing} = context;
  11.108      val (name, _) = #name header;
  11.109      val keywords =
  11.110        fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
  11.111          (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
  11.112  
  11.113 -    val toks = Token.explode keywords text_pos text;
  11.114 -    val spans = Outer_Syntax.parse_spans toks;
  11.115 +    val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
  11.116      val elements = Thy_Syntax.parse_elements keywords spans;
  11.117  
  11.118      fun init () =
  11.119 @@ -282,15 +320,11 @@
  11.120  
  11.121      fun present () =
  11.122        let
  11.123 -        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
  11.124 -        val _ = apply_presentation thy;
  11.125 -      in
  11.126 -        if exists (Toplevel.is_skipped_proof o #2) res then ()
  11.127 -        else
  11.128 -          let val body = Thy_Output.present_thy thy res toks;
  11.129 -          in if document then Present.theory_output text_pos thy body else () end
  11.130 -      end;
  11.131 -
  11.132 +        val segments = (spans ~~ maps Toplevel.join_results results)
  11.133 +          |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
  11.134 +        val context: presentation_context =
  11.135 +          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
  11.136 +      in apply_presentation context thy end;
  11.137    in (thy, present, size text) end;
  11.138  
  11.139  
  11.140 @@ -402,20 +436,13 @@
  11.141  
  11.142  (* use theories *)
  11.143  
  11.144 -fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
  11.145 -  let
  11.146 -    val context =
  11.147 -      {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
  11.148 -        last_timing = last_timing};
  11.149 -    val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
  11.150 +fun use_theories context qualifier master_dir imports =
  11.151 +  let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
  11.152    in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
  11.153  
  11.154  fun use_thy name =
  11.155 -  use_theories
  11.156 -    {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
  11.157 -      last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
  11.158 -      master_dir = Path.current}
  11.159 -    [(name, Position.none)];
  11.160 +  use_theories (default_context ()) Resources.default_qualifier
  11.161 +    Path.current [(name, Position.none)];
  11.162  
  11.163  
  11.164  (* toplevel scripting -- without maintaining database *)
    12.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 14 18:19:35 2018 +0200
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 14 22:23:25 2018 +0200
    12.3 @@ -10,8 +10,8 @@
    12.4    val check_comments: Proof.context -> Symbol_Pos.T list -> unit
    12.5    val output_token: Proof.context -> Token.T -> Latex.text list
    12.6    val output_source: Proof.context -> string -> Latex.text list
    12.7 -  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
    12.8 -    Token.T list -> Latex.text list
    12.9 +  type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
   12.10 +  val present_thy: theory -> segment list -> Latex.text list
   12.11    val pretty_term: Proof.context -> term -> Pretty.T
   12.12    val pretty_thm: Proof.context -> thm -> Pretty.T
   12.13    val lines: Latex.text list -> Latex.text list
   12.14 @@ -338,7 +338,9 @@
   12.15  
   12.16  in
   12.17  
   12.18 -fun present_thy thy command_results toks =
   12.19 +type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
   12.20 +
   12.21 +fun present_thy thy (segments: segment list) =
   12.22    let
   12.23      val keywords = Thy_Header.get_keywords thy;
   12.24  
   12.25 @@ -404,13 +406,18 @@
   12.26        >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
   12.27            make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   12.28  
   12.29 -    val spans = toks
   12.30 +    val spans = segments
   12.31 +      |> maps (Command_Span.content o #span)
   12.32        |> drop_suffix Token.is_space
   12.33        |> Source.of_list
   12.34        |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
   12.35        |> Source.source stopper (Scan.error (Scan.bulk span))
   12.36        |> Source.exhaust;
   12.37  
   12.38 +    val command_results =
   12.39 +      segments |> map_filter (fn {command, state, ...} =>
   12.40 +        if Toplevel.is_ignored command then NONE else SOME (command, state));
   12.41 +
   12.42  
   12.43      (* present commands *)
   12.44  
   12.45 @@ -421,11 +428,11 @@
   12.46          (present_span thy keywords document_tags span st st');
   12.47  
   12.48      fun present _ [] = I
   12.49 -      | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
   12.50 +      | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   12.51    in
   12.52      if length command_results = length spans then
   12.53        ((NONE, []), NONE, true, [], (I, I))
   12.54 -      |> present Toplevel.toplevel (command_results ~~ spans)
   12.55 +      |> present Toplevel.toplevel (spans ~~ command_results)
   12.56        |> present_trailer
   12.57        |> rev
   12.58      else error "Messed-up outer syntax for presentation"
    13.1 --- a/src/Pure/Tools/build.ML	Mon May 14 18:19:35 2018 +0200
    13.2 +++ b/src/Pure/Tools/build.ML	Mon May 14 22:23:25 2018 +0200
    13.3 @@ -113,6 +113,9 @@
    13.4  
    13.5  fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
    13.6    let
    13.7 +    val context =
    13.8 +      {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
    13.9 +        last_timing = last_timing};
   13.10      val condition = space_explode "," (Options.string options "condition");
   13.11      val conds = filter_out (can getenv_strict) condition;
   13.12    in
   13.13 @@ -121,13 +124,7 @@
   13.14          Options.set_default options;
   13.15          Isabelle_Process.init_options ();
   13.16          Future.fork I;
   13.17 -        (Thy_Info.use_theories {
   13.18 -          document = Present.document_enabled (Options.string options "document"),
   13.19 -          symbols = symbols,
   13.20 -          bibtex_entries = bibtex_entries,
   13.21 -          last_timing = last_timing,
   13.22 -          qualifier = qualifier,
   13.23 -          master_dir = master_dir}
   13.24 +        (Thy_Info.use_theories context qualifier master_dir
   13.25          |>
   13.26            (case Options.string options "profiling" of
   13.27              "" => I