--- a/NEWS Mon Jan 08 22:36:02 2018 +0100
+++ b/NEWS Mon Jan 08 23:45:43 2018 +0100
@@ -108,6 +108,10 @@
syntax, antiquotations are interpreted wrt. the presentation context of
the enclosing command.
+* Outside of the inner theory body, the default presentation context is
+theory Pure. Thus elementary antiquotations may be used in markup
+commands (e.g. 'chapter', 'section', 'text') and formal comments.
+
* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).
--- a/src/Pure/Isar/toplevel.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Jan 08 23:45:43 2018 +0100
@@ -16,7 +16,6 @@
val is_proof: state -> bool
val is_skipped_proof: state -> bool
val level: state -> int
- val presentation_context_of: state -> Proof.context
val previous_context_of: state -> Proof.context option
val context_of: state -> Proof.context
val generic_theory_of: state -> generic_theory
@@ -24,6 +23,8 @@
val proof_of: state -> Proof.state
val proof_position_of: state -> int
val end_theory: Position.T -> state -> theory
+ val presentation_context: state -> Proof.context
+ val presentation_state: Proof.context -> state
val pretty_context: state -> Pretty.T list
val pretty_state: state -> Pretty.T list
val string_of_state: state -> string
@@ -154,12 +155,6 @@
fun node_case f g state = cases_node f g (node_of state);
-fun presentation_context_of state =
- (case try node_of state of
- SOME (Theory (_, SOME ctxt)) => ctxt
- | SOME node => context_node node
- | NONE => raise UNDEF);
-
fun previous_context_of (State (_, NONE)) = NONE
| previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
@@ -178,6 +173,30 @@
| end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
+(* presentation context *)
+
+structure Presentation_State = Proof_Data
+(
+ type T = state option;
+ fun init _ = NONE;
+);
+
+fun presentation_context state =
+ (case try node_of state of
+ SOME (Theory (_, SOME ctxt)) => ctxt
+ | SOME node => context_node node
+ | NONE =>
+ (case try Theory.get_pure () of
+ SOME thy => Proof_Context.init_global thy
+ | NONE => raise UNDEF))
+ |> Presentation_State.put (SOME state);
+
+fun presentation_state ctxt =
+ (case Presentation_State.get ctxt of
+ NONE => generic_theory_toplevel (Context.Proof ctxt)
+ | SOME state => state);
+
+
(* print state *)
fun pretty_context state =
@@ -580,7 +599,7 @@
fun transition int tr st =
let
val (st', opt_err) =
- Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
+ Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
(fn () => app int tr st) ();
val opt_err' = opt_err |> Option.map
(fn Runtime.EXCURSION_FAIL exn_info => exn_info
@@ -704,7 +723,7 @@
val (result, result_state) =
State (SOME (Proof (prf', (finish, orig_gthy))), prev)
|> fold_map (element_result keywords) body_elems ||> command end_tr;
- in (Result_List result, presentation_context_of result_state) end))
+ in (Result_List result, presentation_context result_state) end))
#> (fn (res, state') => state' |> put_result (Result_Future res));
val forked_proof =
@@ -717,7 +736,7 @@
|> command (head_tr |> reset_trans |> forked_proof);
val end_result = Result (end_tr, st'');
val result =
- Result_List [head_result, Result.get (presentation_context_of st''), end_result];
+ Result_List [head_result, Result.get (presentation_context st''), end_result];
in (result, st'') end
end;
--- a/src/Pure/ML/ml_file.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/ML/ml_file.ML Mon Jan 08 23:45:43 2018 +0100
@@ -19,9 +19,7 @@
val provide = Resources.provide (src_path, digest);
val source = Input.source true (cat_lines lines) (pos, pos);
- val _ =
- Thy_Output.check_comments (Toplevel.generic_theory_toplevel gthy)
- (Input.source_explode source);
+ val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
val flags =
{SML = SML, exchange = false, redirect = true, verbose = true,
--- a/src/Pure/PIDE/command.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/PIDE/command.ML Mon Jan 08 23:45:43 2018 +0100
@@ -200,13 +200,13 @@
if Exn.is_interrupt exn then Exn.reraise exn
else Runtime.exn_messages exn;
-fun check_cmts span tr st' =
+fun check_cmts ctxt span tr =
Toplevel.setmp_thread_position tr
(fn () =>
(span |> maps (fn tok =>
- check_error (fn () => Thy_Output.check_token_comments st' tok))) @
+ check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @
(Outer_Syntax.side_comments span |> maps (fn tok =>
- check_error (fn () => Thy_Output.output_text st' {markdown = false} (Token.input_of tok)))))
+ check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok)))))
();
fun report tr m =
@@ -239,7 +239,13 @@
val _ = command_indent tr st;
val _ = status tr Markup.running;
val (errs1, result) = run keywords true tr st;
- val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
+ val errs2 =
+ (case result of
+ NONE => []
+ | SOME st' =>
+ (case try Toplevel.presentation_context st' of
+ NONE => []
+ | SOME ctxt' => check_cmts ctxt' span tr));
val errs = errs1 @ errs2;
val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
in
--- a/src/Pure/Thy/document_antiquotations.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Mon Jan 08 23:45:43 2018 +0100
@@ -44,8 +44,8 @@
fun control_antiquotation name s1 s2 =
Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
- (fn {state, ...} =>
- enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
+ (fn {context = ctxt, ...} =>
+ enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
in
@@ -84,7 +84,7 @@
val _ =
Theory.setup
(Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
- (fn {state, context = ctxt, ...} => fn source =>
+ (fn {context = ctxt, ...} => fn source =>
let
val _ =
Context_Position.report ctxt (Input.pos_of source)
@@ -101,7 +101,7 @@
val indentation =
Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
in
- Latex.output_text (maps (Thy_Output.output_token state) toks) |>
+ Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
(if Config.get ctxt Thy_Output.display then
split_lines #> map (prefix indentation) #> cat_lines #>
Latex.environment "isabelle"
@@ -114,11 +114,11 @@
local
fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
- (fn {state, context = ctxt, ...} => fn () =>
+ (fn {context = ctxt, ...} => fn () =>
Thy_Output.output ctxt
[Goal_Display.pretty_goal
(Config.put Goal_Display.show_main_goal main ctxt)
- (#goal (Proof.goal (Toplevel.proof_of state)))]);
+ (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]);
in
--- a/src/Pure/Thy/thy_output.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Jan 08 23:45:43 2018 +0100
@@ -19,15 +19,14 @@
val check_option: Proof.context -> xstring * Position.T -> string
val print_antiquotations: bool -> Proof.context -> unit
val antiquotation: binding -> 'a context_parser ->
- ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
- theory -> theory
+ ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
val boolean: string -> bool
val integer: string -> int
- val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
- val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
- val check_comments: Toplevel.state -> Symbol_Pos.T list -> unit
- val check_token_comments: Toplevel.state -> Token.T -> unit
- val output_token: Toplevel.state -> Token.T -> Latex.text list
+ val eval_antiquote: Proof.context -> Antiquote.text_antiquote -> string
+ val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
+ val check_comments: Proof.context -> Symbol_Pos.T list -> unit
+ val check_token_comments: Proof.context -> Token.T -> unit
+ val output_token: Proof.context -> Token.T -> Latex.text list
val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
Token.T list -> Latex.text list
val pretty_text: Proof.context -> string -> Pretty.T
@@ -39,8 +38,6 @@
val string_of_margin: Proof.context -> Pretty.T -> string
val output: Proof.context -> Pretty.T list -> string
val verbatim_text: Proof.context -> string -> string
- val document_command: {markdown: bool} ->
- (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
end;
structure Thy_Output: THY_OUTPUT =
@@ -74,7 +71,7 @@
structure Antiquotations = Theory_Data
(
type T =
- (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
+ (Token.src -> Proof.context -> string) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
(Name_Space.empty_table Markup.document_antiquotationN,
@@ -97,9 +94,9 @@
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
-fun command src state ctxt =
+fun command src ctxt =
let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
- in f src' state ctxt end;
+ in f src' ctxt end;
fun option ((xname, pos), s) ctxt =
let
@@ -119,9 +116,9 @@
fun antiquotation name scan body =
add_command name
- (fn src => fn state => fn ctxt =>
+ (fn src => fn ctxt =>
let val (x, ctxt') = Token.syntax scan src ctxt
- in body {source = src, state = state, context = ctxt'} x end);
+ in body {source = src, context = ctxt'} x end);
@@ -166,12 +163,12 @@
local
-fun eval_antiq state (opts, src) =
+fun eval_antiq ctxt (opts, src) =
let
- val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
+ val preview_ctxt = fold option opts ctxt;
val print_ctxt = Context_Position.set_visible false preview_ctxt;
- fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
+ fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
val _ = cmd preview_ctxt;
val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
@@ -179,18 +176,12 @@
in
fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
- | eval_antiquote state (Antiquote.Control {name, body, ...}) =
- eval_antiq state
+ | eval_antiquote ctxt (Antiquote.Control {name, body, ...}) =
+ eval_antiq ctxt
([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
- | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
- let
- val keywords =
- (case try Toplevel.presentation_context_of state of
- SOME ctxt => Thy_Header.get_keywords' ctxt
- | NONE =>
- error ("Unknown context -- cannot expand document antiquotations" ^
- Position.here pos));
- in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end;
+ | eval_antiquote ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
+ let val keywords = Thy_Header.get_keywords' ctxt;
+ in eval_antiq ctxt (Token.read_antiq keywords antiq (body, pos)) end;
end;
@@ -200,23 +191,15 @@
(* output text *)
-fun output_text state {markdown} source =
+fun output_text ctxt {markdown} source =
let
- val is_reported =
- (case try Toplevel.context_of state of
- SOME ctxt => Context_Position.is_visible ctxt
- | NONE => true);
-
val pos = Input.pos_of source;
val syms = Input.source_explode source;
- val _ =
- if is_reported then
- Position.report pos (Markup.language_document (Input.is_delimited source))
- else ();
+ val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
val output_antiquotes =
- map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
+ map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant])));
fun output_line line =
(if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -228,20 +211,20 @@
Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
in
- if Toplevel.is_skipped_proof state then []
+ if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
then
let
val ants = Antiquote.parse pos syms;
val reports = Antiquote.antiq_reports ants;
val blocks = Markdown.read_antiquotes ants;
- val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
+ val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
in output_blocks blocks end
else
let
val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
val reports = Antiquote.antiq_reports ants;
- val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
+ val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
in output_antiquotes ants end
end;
@@ -261,10 +244,10 @@
| Antiquote.Antiq {body, ...} =>
Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
-fun output_symbols_comment state {antiq} (is_comment, syms) =
+fun output_symbols_comment ctxt {antiq} (is_comment, syms) =
if is_comment then
Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
- (output_text state {markdown = false}
+ (output_text ctxt {markdown = false}
(Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
else if antiq then maps output_symbols_antiq (Antiquote.parse (#1 (Symbol_Pos.range syms)) syms)
else output_symbols syms;
@@ -282,14 +265,14 @@
in
-fun output_body state antiq bg en syms =
+fun output_body ctxt antiq bg en syms =
(case read_symbols_comment syms of
- SOME res => maps (output_symbols_comment state {antiq = antiq}) res
+ SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
| NONE => output_symbols syms) |> Latex.enclose_body bg en
-and output_token state tok =
+and output_token ctxt tok =
let
fun output antiq bg en =
- output_body state antiq bg en (Input.source_explode (Token.input_of tok));
+ output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
in
(case Token.kind_of tok of
Token.Comment => []
@@ -305,13 +288,13 @@
| _ => output false "" "")
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
-fun check_comments state =
+fun check_comments ctxt =
read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
- (output_symbols_comment state {antiq = false} (is_comment, syms);
- if is_comment then check_comments state syms else ()));
+ (output_symbols_comment ctxt {antiq = false} (is_comment, syms);
+ if is_comment then check_comments ctxt syms else ()));
-fun check_token_comments state tok =
- check_comments state (Input.source_explode (Token.input_of tok));
+fun check_token_comments ctxt tok =
+ check_comments ctxt (Input.source_explode (Token.input_of tok));
end;
@@ -339,17 +322,17 @@
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
-fun present_token state tok =
+fun present_token ctxt tok =
(case tok of
Ignore_Token => []
- | Basic_Token tok => output_token state tok
+ | Basic_Token tok => output_token ctxt tok
| Markup_Token (cmd, source) =>
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
- (output_text state {markdown = false} source)
+ (output_text ctxt {markdown = false} source)
| Markup_Env_Token (cmd, source) =>
- [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
+ [Latex.environment_block ("isamarkup" ^ cmd) (output_text ctxt {markdown = true} source)]
| Raw_Token source =>
- Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
+ Latex.string "%\n" :: output_text ctxt {markdown = true} source @ [Latex.string "\n"]);
(* command spans *)
@@ -392,11 +375,14 @@
in
-fun present_span keywords document_tags span state state'
+fun present_span thy keywords document_tags span state state'
(tag_stack, active_tag, newline, latex, present_cont) =
let
+ val ctxt' =
+ Toplevel.presentation_context state'
+ handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN);
val present = fold (fn (tok, (flag, 0)) =>
- fold cons (present_token state' tok)
+ fold cons (present_token ctxt' tok)
#> cons (Latex.string flag)
| _ => I);
@@ -569,7 +555,7 @@
fun present_command tr span st st' =
Toplevel.setmp_thread_position tr
- (present_span keywords document_tags span st st');
+ (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;
@@ -744,17 +730,4 @@
end;
-
-
-(** document command **)
-
-fun document_command {markdown} (loc, txt) =
- Toplevel.keep (fn state =>
- (case loc of
- NONE => ignore (output_text state {markdown = markdown} txt)
- | SOME (_, pos) =>
- error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
- Toplevel.present_local_theory loc (fn state =>
- ignore (output_text state {markdown = markdown} txt));
-
end;
--- a/src/Pure/Tools/debugger.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/Tools/debugger.ML Mon Jan 08 23:45:43 2018 +0100
@@ -276,7 +276,7 @@
if Command.eval_finished eval then
let
val st = Command.eval_result_state eval;
- val ctxt = Toplevel.presentation_context_of st
+ val ctxt = Toplevel.presentation_context st
handle Toplevel.UNDEF => err ();
in
(case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
--- a/src/Pure/Tools/rail.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/Tools/rail.ML Mon Jan 08 23:45:43 2018 +0100
@@ -17,7 +17,7 @@
Terminal of bool * string |
Antiquote of bool * Antiquote.antiq
val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
- val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
+ val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> string
end;
structure Rail: RAIL =
@@ -330,9 +330,9 @@
in
-fun output_rules state rules =
+fun output_rules ctxt rules =
let
- val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
+ val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq;
fun output_text b s =
Output.output s
|> b ? enclose "\\isakeyword{" "}"
@@ -375,7 +375,7 @@
val _ = Theory.setup
(Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
- (fn {state, context, ...} => output_rules state o read context));
+ (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
end;
--- a/src/Pure/pure_syn.ML Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/pure_syn.ML Mon Jan 08 23:45:43 2018 +0100
@@ -7,6 +7,8 @@
signature PURE_SYN =
sig
+ val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
+ Toplevel.transition -> Toplevel.transition
val bootstrap_thy: theory
end;
@@ -15,47 +17,52 @@
val semi = Scan.option (Parse.$$$ ";");
+fun document_command {markdown} (loc, txt) =
+ Toplevel.keep (fn state =>
+ (case loc of
+ NONE =>
+ ignore (Thy_Output.output_text
+ (Toplevel.presentation_context state) {markdown = markdown} txt)
+ | SOME (_, pos) =>
+ error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
+ Toplevel.present_local_theory loc (fn state =>
+ ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt));
+
val _ =
Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("section", \<^here>) "section heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
- (Parse.opt_target -- Parse.document_source --| semi
- >> Thy_Output.document_command {markdown = false});
+ (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});
val _ =
Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+ (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
val _ =
Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+ (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
val _ =
Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
- (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
+ (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});
val _ =
Outer_Syntax.command ("theory", \<^here>) "begin theory"