theory Pure is default presentation context;
authorwenzelm
Mon Jan 08 23:45:43 2018 +0100 (17 months ago ago)
changeset 67381146757999c8d
parent 67380 8bef51521f21
child 67382 39e4668ded4f
theory Pure is default presentation context;
NEWS
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_file.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/debugger.ML
src/Pure/Tools/rail.ML
src/Pure/pure_syn.ML
     1.1 --- a/NEWS	Mon Jan 08 22:36:02 2018 +0100
     1.2 +++ b/NEWS	Mon Jan 08 23:45:43 2018 +0100
     1.3 @@ -108,6 +108,10 @@
     1.4  syntax, antiquotations are interpreted wrt. the presentation context of
     1.5  the enclosing command.
     1.6  
     1.7 +* Outside of the inner theory body, the default presentation context is
     1.8 +theory Pure. Thus elementary antiquotations may be used in markup
     1.9 +commands (e.g. 'chapter', 'section', 'text') and formal comments.
    1.10 +
    1.11  * System option "document_tags" specifies a default for otherwise
    1.12  untagged commands. This is occasionally useful to control the global
    1.13  visibility of commands via session options (e.g. in ROOT).
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 08 22:36:02 2018 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 08 23:45:43 2018 +0100
     2.3 @@ -16,7 +16,6 @@
     2.4    val is_proof: state -> bool
     2.5    val is_skipped_proof: state -> bool
     2.6    val level: state -> int
     2.7 -  val presentation_context_of: state -> Proof.context
     2.8    val previous_context_of: state -> Proof.context option
     2.9    val context_of: state -> Proof.context
    2.10    val generic_theory_of: state -> generic_theory
    2.11 @@ -24,6 +23,8 @@
    2.12    val proof_of: state -> Proof.state
    2.13    val proof_position_of: state -> int
    2.14    val end_theory: Position.T -> state -> theory
    2.15 +  val presentation_context: state -> Proof.context
    2.16 +  val presentation_state: Proof.context -> state
    2.17    val pretty_context: state -> Pretty.T list
    2.18    val pretty_state: state -> Pretty.T list
    2.19    val string_of_state: state -> string
    2.20 @@ -154,12 +155,6 @@
    2.21  
    2.22  fun node_case f g state = cases_node f g (node_of state);
    2.23  
    2.24 -fun presentation_context_of state =
    2.25 -  (case try node_of state of
    2.26 -    SOME (Theory (_, SOME ctxt)) => ctxt
    2.27 -  | SOME node => context_node node
    2.28 -  | NONE => raise UNDEF);
    2.29 -
    2.30  fun previous_context_of (State (_, NONE)) = NONE
    2.31    | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
    2.32  
    2.33 @@ -178,6 +173,30 @@
    2.34    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
    2.35  
    2.36  
    2.37 +(* presentation context *)
    2.38 +
    2.39 +structure Presentation_State = Proof_Data
    2.40 +(
    2.41 +  type T = state option;
    2.42 +  fun init _ = NONE;
    2.43 +);
    2.44 +
    2.45 +fun presentation_context state =
    2.46 +  (case try node_of state of
    2.47 +    SOME (Theory (_, SOME ctxt)) => ctxt
    2.48 +  | SOME node => context_node node
    2.49 +  | NONE =>
    2.50 +      (case try Theory.get_pure () of
    2.51 +        SOME thy => Proof_Context.init_global thy
    2.52 +      | NONE => raise UNDEF))
    2.53 +  |> Presentation_State.put (SOME state);
    2.54 +
    2.55 +fun presentation_state ctxt =
    2.56 +  (case Presentation_State.get ctxt of
    2.57 +    NONE => generic_theory_toplevel (Context.Proof ctxt)
    2.58 +  | SOME state => state);
    2.59 +
    2.60 +
    2.61  (* print state *)
    2.62  
    2.63  fun pretty_context state =
    2.64 @@ -580,7 +599,7 @@
    2.65  fun transition int tr st =
    2.66    let
    2.67      val (st', opt_err) =
    2.68 -      Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
    2.69 +      Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
    2.70          (fn () => app int tr st) ();
    2.71      val opt_err' = opt_err |> Option.map
    2.72        (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    2.73 @@ -704,7 +723,7 @@
    2.74                        val (result, result_state) =
    2.75                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    2.76                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
    2.77 -                    in (Result_List result, presentation_context_of result_state) end))
    2.78 +                    in (Result_List result, presentation_context result_state) end))
    2.79                #> (fn (res, state') => state' |> put_result (Result_Future res));
    2.80  
    2.81              val forked_proof =
    2.82 @@ -717,7 +736,7 @@
    2.83                |> command (head_tr |> reset_trans |> forked_proof);
    2.84              val end_result = Result (end_tr, st'');
    2.85              val result =
    2.86 -              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
    2.87 +              Result_List [head_result, Result.get (presentation_context st''), end_result];
    2.88            in (result, st'') end
    2.89        end;
    2.90  
     3.1 --- a/src/Pure/ML/ml_file.ML	Mon Jan 08 22:36:02 2018 +0100
     3.2 +++ b/src/Pure/ML/ml_file.ML	Mon Jan 08 23:45:43 2018 +0100
     3.3 @@ -19,9 +19,7 @@
     3.4      val provide = Resources.provide (src_path, digest);
     3.5      val source = Input.source true (cat_lines lines) (pos, pos);
     3.6  
     3.7 -    val _ =
     3.8 -      Thy_Output.check_comments (Toplevel.generic_theory_toplevel gthy)
     3.9 -        (Input.source_explode source);
    3.10 +    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
    3.11  
    3.12      val flags =
    3.13        {SML = SML, exchange = false, redirect = true, verbose = true,
     4.1 --- a/src/Pure/PIDE/command.ML	Mon Jan 08 22:36:02 2018 +0100
     4.2 +++ b/src/Pure/PIDE/command.ML	Mon Jan 08 23:45:43 2018 +0100
     4.3 @@ -200,13 +200,13 @@
     4.4      if Exn.is_interrupt exn then Exn.reraise exn
     4.5      else Runtime.exn_messages exn;
     4.6  
     4.7 -fun check_cmts span tr st' =
     4.8 +fun check_cmts ctxt span tr =
     4.9    Toplevel.setmp_thread_position tr
    4.10      (fn () =>
    4.11        (span |> maps (fn tok =>
    4.12 -        check_error (fn () => Thy_Output.check_token_comments st' tok))) @
    4.13 +        check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @
    4.14        (Outer_Syntax.side_comments span |> maps (fn tok =>
    4.15 -        check_error (fn () => Thy_Output.output_text st' {markdown = false} (Token.input_of tok)))))
    4.16 +        check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok)))))
    4.17      ();
    4.18  
    4.19  fun report tr m =
    4.20 @@ -239,7 +239,13 @@
    4.21      val _ = command_indent tr st;
    4.22      val _ = status tr Markup.running;
    4.23      val (errs1, result) = run keywords true tr st;
    4.24 -    val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
    4.25 +    val errs2 =
    4.26 +      (case result of
    4.27 +        NONE => []
    4.28 +      | SOME st' =>
    4.29 +          (case try Toplevel.presentation_context st' of
    4.30 +            NONE => []
    4.31 +          | SOME ctxt' => check_cmts ctxt' span tr));
    4.32      val errs = errs1 @ errs2;
    4.33      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
    4.34    in
     5.1 --- a/src/Pure/Thy/document_antiquotations.ML	Mon Jan 08 22:36:02 2018 +0100
     5.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Mon Jan 08 23:45:43 2018 +0100
     5.3 @@ -44,8 +44,8 @@
     5.4  
     5.5  fun control_antiquotation name s1 s2 =
     5.6    Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
     5.7 -    (fn {state, ...} =>
     5.8 -      enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
     5.9 +    (fn {context = ctxt, ...} =>
    5.10 +      enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
    5.11  
    5.12  in
    5.13  
    5.14 @@ -84,7 +84,7 @@
    5.15  val _ =
    5.16    Theory.setup
    5.17      (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
    5.18 -      (fn {state, context = ctxt, ...} => fn source =>
    5.19 +      (fn {context = ctxt, ...} => fn source =>
    5.20          let
    5.21            val _ =
    5.22              Context_Position.report ctxt (Input.pos_of source)
    5.23 @@ -101,7 +101,7 @@
    5.24            val indentation =
    5.25              Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
    5.26          in
    5.27 -          Latex.output_text (maps (Thy_Output.output_token state) toks) |>
    5.28 +          Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
    5.29             (if Config.get ctxt Thy_Output.display then
    5.30                split_lines #> map (prefix indentation) #> cat_lines #>
    5.31                Latex.environment "isabelle"
    5.32 @@ -114,11 +114,11 @@
    5.33  local
    5.34  
    5.35  fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
    5.36 -  (fn {state, context = ctxt, ...} => fn () =>
    5.37 +  (fn {context = ctxt, ...} => fn () =>
    5.38      Thy_Output.output ctxt
    5.39        [Goal_Display.pretty_goal
    5.40          (Config.put Goal_Display.show_main_goal main ctxt)
    5.41 -        (#goal (Proof.goal (Toplevel.proof_of state)))]);
    5.42 +        (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]);
    5.43  
    5.44  in
    5.45  
     6.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jan 08 22:36:02 2018 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jan 08 23:45:43 2018 +0100
     6.3 @@ -19,15 +19,14 @@
     6.4    val check_option: Proof.context -> xstring * Position.T -> string
     6.5    val print_antiquotations: bool -> Proof.context -> unit
     6.6    val antiquotation: binding -> 'a context_parser ->
     6.7 -    ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
     6.8 -      theory -> theory
     6.9 +    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
    6.10    val boolean: string -> bool
    6.11    val integer: string -> int
    6.12 -  val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
    6.13 -  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
    6.14 -  val check_comments: Toplevel.state -> Symbol_Pos.T list -> unit
    6.15 -  val check_token_comments: Toplevel.state -> Token.T -> unit
    6.16 -  val output_token: Toplevel.state -> Token.T -> Latex.text list
    6.17 +  val eval_antiquote: Proof.context -> Antiquote.text_antiquote -> string
    6.18 +  val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
    6.19 +  val check_comments: Proof.context -> Symbol_Pos.T list -> unit
    6.20 +  val check_token_comments: Proof.context -> Token.T -> unit
    6.21 +  val output_token: Proof.context -> Token.T -> Latex.text list
    6.22    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
    6.23      Token.T list -> Latex.text list
    6.24    val pretty_text: Proof.context -> string -> Pretty.T
    6.25 @@ -39,8 +38,6 @@
    6.26    val string_of_margin: Proof.context -> Pretty.T -> string
    6.27    val output: Proof.context -> Pretty.T list -> string
    6.28    val verbatim_text: Proof.context -> string -> string
    6.29 -  val document_command: {markdown: bool} ->
    6.30 -    (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
    6.31  end;
    6.32  
    6.33  structure Thy_Output: THY_OUTPUT =
    6.34 @@ -74,7 +71,7 @@
    6.35  structure Antiquotations = Theory_Data
    6.36  (
    6.37    type T =
    6.38 -    (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    6.39 +    (Token.src -> Proof.context -> string) Name_Space.table *
    6.40        (string -> Proof.context -> Proof.context) Name_Space.table;
    6.41    val empty : T =
    6.42      (Name_Space.empty_table Markup.document_antiquotationN,
    6.43 @@ -97,9 +94,9 @@
    6.44  
    6.45  fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
    6.46  
    6.47 -fun command src state ctxt =
    6.48 +fun command src ctxt =
    6.49    let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
    6.50 -  in f src' state ctxt end;
    6.51 +  in f src' ctxt end;
    6.52  
    6.53  fun option ((xname, pos), s) ctxt =
    6.54    let
    6.55 @@ -119,9 +116,9 @@
    6.56  
    6.57  fun antiquotation name scan body =
    6.58    add_command name
    6.59 -    (fn src => fn state => fn ctxt =>
    6.60 +    (fn src => fn ctxt =>
    6.61        let val (x, ctxt') = Token.syntax scan src ctxt
    6.62 -      in body {source = src, state = state, context = ctxt'} x end);
    6.63 +      in body {source = src, context = ctxt'} x end);
    6.64  
    6.65  
    6.66  
    6.67 @@ -166,12 +163,12 @@
    6.68  
    6.69  local
    6.70  
    6.71 -fun eval_antiq state (opts, src) =
    6.72 +fun eval_antiq ctxt (opts, src) =
    6.73    let
    6.74 -    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    6.75 +    val preview_ctxt = fold option opts ctxt;
    6.76      val print_ctxt = Context_Position.set_visible false preview_ctxt;
    6.77  
    6.78 -    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    6.79 +    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
    6.80      val _ = cmd preview_ctxt;
    6.81      val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
    6.82    in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    6.83 @@ -179,18 +176,12 @@
    6.84  in
    6.85  
    6.86  fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
    6.87 -  | eval_antiquote state (Antiquote.Control {name, body, ...}) =
    6.88 -      eval_antiq state
    6.89 +  | eval_antiquote ctxt (Antiquote.Control {name, body, ...}) =
    6.90 +      eval_antiq ctxt
    6.91          ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
    6.92 -  | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
    6.93 -      let
    6.94 -        val keywords =
    6.95 -          (case try Toplevel.presentation_context_of state of
    6.96 -            SOME ctxt => Thy_Header.get_keywords' ctxt
    6.97 -          | NONE =>
    6.98 -              error ("Unknown context -- cannot expand document antiquotations" ^
    6.99 -                Position.here pos));
   6.100 -      in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end;
   6.101 +  | eval_antiquote ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
   6.102 +      let val keywords = Thy_Header.get_keywords' ctxt;
   6.103 +      in eval_antiq ctxt (Token.read_antiq keywords antiq (body, pos)) end;
   6.104  
   6.105  end;
   6.106  
   6.107 @@ -200,23 +191,15 @@
   6.108  
   6.109  (* output text *)
   6.110  
   6.111 -fun output_text state {markdown} source =
   6.112 +fun output_text ctxt {markdown} source =
   6.113    let
   6.114 -    val is_reported =
   6.115 -      (case try Toplevel.context_of state of
   6.116 -        SOME ctxt => Context_Position.is_visible ctxt
   6.117 -      | NONE => true);
   6.118 -
   6.119      val pos = Input.pos_of source;
   6.120      val syms = Input.source_explode source;
   6.121  
   6.122 -    val _ =
   6.123 -      if is_reported then
   6.124 -        Position.report pos (Markup.language_document (Input.is_delimited source))
   6.125 -      else ();
   6.126 +    val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
   6.127  
   6.128      val output_antiquotes =
   6.129 -      map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
   6.130 +      map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant])));
   6.131  
   6.132      fun output_line line =
   6.133        (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
   6.134 @@ -228,20 +211,20 @@
   6.135            Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
   6.136      and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
   6.137    in
   6.138 -    if Toplevel.is_skipped_proof state then []
   6.139 +    if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
   6.140      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   6.141      then
   6.142        let
   6.143          val ants = Antiquote.parse pos syms;
   6.144          val reports = Antiquote.antiq_reports ants;
   6.145          val blocks = Markdown.read_antiquotes ants;
   6.146 -        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
   6.147 +        val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
   6.148        in output_blocks blocks end
   6.149      else
   6.150        let
   6.151          val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
   6.152          val reports = Antiquote.antiq_reports ants;
   6.153 -        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
   6.154 +        val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
   6.155        in output_antiquotes ants end
   6.156    end;
   6.157  
   6.158 @@ -261,10 +244,10 @@
   6.159      | Antiquote.Antiq {body, ...} =>
   6.160          Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
   6.161  
   6.162 -fun output_symbols_comment state {antiq} (is_comment, syms) =
   6.163 +fun output_symbols_comment ctxt {antiq} (is_comment, syms) =
   6.164    if is_comment then
   6.165      Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
   6.166 -      (output_text state {markdown = false}
   6.167 +      (output_text ctxt {markdown = false}
   6.168          (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
   6.169    else if antiq then maps output_symbols_antiq (Antiquote.parse (#1 (Symbol_Pos.range syms)) syms)
   6.170    else output_symbols syms;
   6.171 @@ -282,14 +265,14 @@
   6.172  
   6.173  in
   6.174  
   6.175 -fun output_body state antiq bg en syms =
   6.176 +fun output_body ctxt antiq bg en syms =
   6.177    (case read_symbols_comment syms of
   6.178 -    SOME res => maps (output_symbols_comment state {antiq = antiq}) res
   6.179 +    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
   6.180    | NONE => output_symbols syms) |> Latex.enclose_body bg en
   6.181 -and output_token state tok =
   6.182 +and output_token ctxt tok =
   6.183    let
   6.184      fun output antiq bg en =
   6.185 -      output_body state antiq bg en (Input.source_explode (Token.input_of tok));
   6.186 +      output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   6.187    in
   6.188      (case Token.kind_of tok of
   6.189        Token.Comment => []
   6.190 @@ -305,13 +288,13 @@
   6.191      | _ => output false "" "")
   6.192    end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
   6.193  
   6.194 -fun check_comments state =
   6.195 +fun check_comments ctxt =
   6.196    read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
   6.197 -    (output_symbols_comment state {antiq = false} (is_comment, syms);
   6.198 -     if is_comment then check_comments state syms else ()));
   6.199 +    (output_symbols_comment ctxt {antiq = false} (is_comment, syms);
   6.200 +     if is_comment then check_comments ctxt syms else ()));
   6.201  
   6.202 -fun check_token_comments state tok =
   6.203 -  check_comments state (Input.source_explode (Token.input_of tok));
   6.204 +fun check_token_comments ctxt tok =
   6.205 +  check_comments ctxt (Input.source_explode (Token.input_of tok));
   6.206  
   6.207  end;
   6.208  
   6.209 @@ -339,17 +322,17 @@
   6.210  val blank_token = basic_token Token.is_blank;
   6.211  val newline_token = basic_token Token.is_newline;
   6.212  
   6.213 -fun present_token state tok =
   6.214 +fun present_token ctxt tok =
   6.215    (case tok of
   6.216      Ignore_Token => []
   6.217 -  | Basic_Token tok => output_token state tok
   6.218 +  | Basic_Token tok => output_token ctxt tok
   6.219    | Markup_Token (cmd, source) =>
   6.220        Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
   6.221 -        (output_text state {markdown = false} source)
   6.222 +        (output_text ctxt {markdown = false} source)
   6.223    | Markup_Env_Token (cmd, source) =>
   6.224 -      [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
   6.225 +      [Latex.environment_block ("isamarkup" ^ cmd) (output_text ctxt {markdown = true} source)]
   6.226    | Raw_Token source =>
   6.227 -      Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
   6.228 +      Latex.string "%\n" :: output_text ctxt {markdown = true} source @ [Latex.string "\n"]);
   6.229  
   6.230  
   6.231  (* command spans *)
   6.232 @@ -392,11 +375,14 @@
   6.233  
   6.234  in
   6.235  
   6.236 -fun present_span keywords document_tags span state state'
   6.237 +fun present_span thy keywords document_tags span state state'
   6.238      (tag_stack, active_tag, newline, latex, present_cont) =
   6.239    let
   6.240 +    val ctxt' =
   6.241 +      Toplevel.presentation_context state'
   6.242 +        handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN);
   6.243      val present = fold (fn (tok, (flag, 0)) =>
   6.244 -        fold cons (present_token state' tok)
   6.245 +        fold cons (present_token ctxt' tok)
   6.246          #> cons (Latex.string flag)
   6.247        | _ => I);
   6.248  
   6.249 @@ -569,7 +555,7 @@
   6.250  
   6.251      fun present_command tr span st st' =
   6.252        Toplevel.setmp_thread_position tr
   6.253 -        (present_span keywords document_tags span st st');
   6.254 +        (present_span thy keywords document_tags span st st');
   6.255  
   6.256      fun present _ [] = I
   6.257        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
   6.258 @@ -744,17 +730,4 @@
   6.259  
   6.260  end;
   6.261  
   6.262 -
   6.263 -
   6.264 -(** document command **)
   6.265 -
   6.266 -fun document_command {markdown} (loc, txt) =
   6.267 -  Toplevel.keep (fn state =>
   6.268 -    (case loc of
   6.269 -      NONE => ignore (output_text state {markdown = markdown} txt)
   6.270 -    | SOME (_, pos) =>
   6.271 -        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   6.272 -  Toplevel.present_local_theory loc (fn state =>
   6.273 -    ignore (output_text state {markdown = markdown} txt));
   6.274 -
   6.275  end;
     7.1 --- a/src/Pure/Tools/debugger.ML	Mon Jan 08 22:36:02 2018 +0100
     7.2 +++ b/src/Pure/Tools/debugger.ML	Mon Jan 08 23:45:43 2018 +0100
     7.3 @@ -276,7 +276,7 @@
     7.4              if Command.eval_finished eval then
     7.5                let
     7.6                  val st = Command.eval_result_state eval;
     7.7 -                val ctxt = Toplevel.presentation_context_of st
     7.8 +                val ctxt = Toplevel.presentation_context st
     7.9                    handle Toplevel.UNDEF => err ();
    7.10                in
    7.11                  (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
     8.1 --- a/src/Pure/Tools/rail.ML	Mon Jan 08 22:36:02 2018 +0100
     8.2 +++ b/src/Pure/Tools/rail.ML	Mon Jan 08 23:45:43 2018 +0100
     8.3 @@ -17,7 +17,7 @@
     8.4      Terminal of bool * string |
     8.5      Antiquote of bool * Antiquote.antiq
     8.6    val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
     8.7 -  val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
     8.8 +  val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> string
     8.9  end;
    8.10  
    8.11  structure Rail: RAIL =
    8.12 @@ -330,9 +330,9 @@
    8.13  
    8.14  in
    8.15  
    8.16 -fun output_rules state rules =
    8.17 +fun output_rules ctxt rules =
    8.18    let
    8.19 -    val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
    8.20 +    val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq;
    8.21      fun output_text b s =
    8.22        Output.output s
    8.23        |> b ? enclose "\\isakeyword{" "}"
    8.24 @@ -375,7 +375,7 @@
    8.25  
    8.26  val _ = Theory.setup
    8.27    (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
    8.28 -    (fn {state, context, ...} => output_rules state o read context));
    8.29 +    (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
    8.30  
    8.31  end;
    8.32  
     9.1 --- a/src/Pure/pure_syn.ML	Mon Jan 08 22:36:02 2018 +0100
     9.2 +++ b/src/Pure/pure_syn.ML	Mon Jan 08 23:45:43 2018 +0100
     9.3 @@ -7,6 +7,8 @@
     9.4  
     9.5  signature PURE_SYN =
     9.6  sig
     9.7 +  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
     9.8 +    Toplevel.transition -> Toplevel.transition
     9.9    val bootstrap_thy: theory
    9.10  end;
    9.11  
    9.12 @@ -15,47 +17,52 @@
    9.13  
    9.14  val semi = Scan.option (Parse.$$$ ";");
    9.15  
    9.16 +fun document_command {markdown} (loc, txt) =
    9.17 +  Toplevel.keep (fn state =>
    9.18 +    (case loc of
    9.19 +      NONE =>
    9.20 +        ignore (Thy_Output.output_text
    9.21 +          (Toplevel.presentation_context state) {markdown = markdown} txt)
    9.22 +    | SOME (_, pos) =>
    9.23 +        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
    9.24 +  Toplevel.present_local_theory loc (fn state =>
    9.25 +    ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt));
    9.26 +
    9.27  val _ =
    9.28    Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
    9.29 -    (Parse.opt_target -- Parse.document_source --| semi
    9.30 -      >> Thy_Output.document_command {markdown = false});
    9.31 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.32  
    9.33  val _ =
    9.34    Outer_Syntax.command ("section", \<^here>) "section heading"
    9.35 -    (Parse.opt_target -- Parse.document_source --| semi
    9.36 -      >> Thy_Output.document_command {markdown = false});
    9.37 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.38  
    9.39  val _ =
    9.40    Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
    9.41 -    (Parse.opt_target -- Parse.document_source --| semi
    9.42 -      >> Thy_Output.document_command {markdown = false});
    9.43 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.44  
    9.45  val _ =
    9.46    Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
    9.47 -    (Parse.opt_target -- Parse.document_source --| semi
    9.48 -      >> Thy_Output.document_command {markdown = false});
    9.49 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.50  
    9.51  val _ =
    9.52    Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
    9.53 -    (Parse.opt_target -- Parse.document_source --| semi
    9.54 -      >> Thy_Output.document_command {markdown = false});
    9.55 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.56  
    9.57  val _ =
    9.58    Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
    9.59 -    (Parse.opt_target -- Parse.document_source --| semi
    9.60 -      >> Thy_Output.document_command {markdown = false});
    9.61 +    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
    9.62  
    9.63  val _ =
    9.64    Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
    9.65 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    9.66 +    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    9.67  
    9.68  val _ =
    9.69    Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
    9.70 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    9.71 +    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    9.72  
    9.73  val _ =
    9.74    Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
    9.75 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    9.76 +    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
    9.77  
    9.78  val _ =
    9.79    Outer_Syntax.command ("theory", \<^here>) "begin theory"