# HG changeset patch # User wenzelm # Date 1515451543 -3600 # Node ID 146757999c8da0867702c5c684649cd9a4819f39 # Parent 8bef51521f217e2f192242795f748bbf0c28e704 theory Pure is default presentation context; diff -r 8bef51521f21 -r 146757999c8d NEWS --- 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). diff -r 8bef51521f21 -r 146757999c8d src/Pure/Isar/toplevel.ML --- 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; diff -r 8bef51521f21 -r 146757999c8d src/Pure/ML/ml_file.ML --- 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, diff -r 8bef51521f21 -r 146757999c8d src/Pure/PIDE/command.ML --- 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 diff -r 8bef51521f21 -r 146757999c8d src/Pure/Thy/document_antiquotations.ML --- 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>\theory_text\ (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 diff -r 8bef51521f21 -r 146757999c8d src/Pure/Thy/thy_output.ML --- 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; diff -r 8bef51521f21 -r 146757999c8d src/Pure/Tools/debugger.ML --- 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 diff -r 8bef51521f21 -r 146757999c8d src/Pure/Tools/rail.ML --- 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>\rail\ (Scan.lift Args.text_input) - (fn {state, context, ...} => output_rules state o read context)); + (fn {context = ctxt, ...} => output_rules ctxt o read ctxt)); end; diff -r 8bef51521f21 -r 146757999c8d src/Pure/pure_syn.ML --- 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"