# HG changeset patch # User wenzelm # Date 1515508812 -3600 # Node ID 998e01d6f8fdb7f4fb48a601aa8e16b6b6ae0286 # Parent deb9b028325926dbc05f7e375708a50974b59564 clarified modules; diff -r deb9b0283259 -r 998e01d6f8fd src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Doc/Main/Main_Doc.thy Tue Jan 09 15:40:12 2018 +0100 @@ -10,7 +10,7 @@ else error "term_type_only: type mismatch"; Syntax.pretty_typ ctxt T) in - Thy_Output.antiquotation @{binding term_type_only} + Document_Antiquotation.setup @{binding term_type_only} (Args.term -- Args.typ_abbrev) (fn {source, context = ctxt, ...} => fn arg => Thy_Output.output ctxt @@ -18,7 +18,7 @@ end \ setup \ - Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single) + Document_Antiquotation.setup @{binding expanded_typ} (Args.typ >> single) (fn {source, context, ...} => Thy_Output.output context o Thy_Output.maybe_pretty_source Syntax.pretty_typ context source) \ diff -r deb9b0283259 -r 998e01d6f8fd src/Doc/Prog_Prove/LaTeXsugar.thy --- a/src/Doc/Prog_Prove/LaTeXsugar.thy Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Tue Jan 09 15:40:12 2018 +0100 @@ -51,7 +51,7 @@ Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end in - Thy_Output.antiquotation @{binding "const_typ"} + Document_Antiquotation.setup @{binding "const_typ"} (Scan.lift Args.embedded_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt diff -r deb9b0283259 -r 998e01d6f8fd src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Doc/antiquote_setup.ML Tue Jan 09 15:40:12 2018 +0100 @@ -73,7 +73,7 @@ fun prep_ml source = (Input.source_content source, ML_Lex.read_source false source); -fun index_ml name kind ml = Thy_Output.antiquotation name +fun index_ml name kind ml = Document_Antiquotation.setup name (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input))) (fn {context = ctxt, ...} => fn (source1, opt_source2) => let @@ -119,17 +119,18 @@ (* named theorems *) val _ = - Theory.setup (Thy_Output.antiquotation @{binding named_thms} + Theory.setup (Document_Antiquotation.setup @{binding named_thms} (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) (fn {context = ctxt, ...} => map (apfst (Thy_Output.pretty_thm ctxt)) - #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) - #> (if Config.get ctxt Thy_Output.display + #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes + then map (apfst Pretty.quote) else I) + #> (if Config.get ctxt Document_Antiquotation.thy_output_display then map (fn (p, name) => Output.output (Thy_Output.string_of_margin ctxt - (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ + (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^ "\\rulename{" ^ Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}") #> space_implode "\\par\\smallskip%\n" @@ -160,7 +161,7 @@ val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = - Thy_Output.antiquotation + Document_Antiquotation.setup (binding |> Binding.map_name (fn name => name ^ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) @@ -204,8 +205,8 @@ entity_antiqs no_check "" @{binding fact} #> entity_antiqs no_check "" @{binding variable} #> entity_antiqs no_check "" @{binding case} #> - entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #> - entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #> + entity_antiqs Document_Antiquotation.check "" @{binding antiquotation} #> + entity_antiqs Document_Antiquotation.check_option "" @{binding antiquotation_option} #> entity_antiqs no_check "isasystem" @{binding setting} #> entity_antiqs check_system_option "isasystem" @{binding system_option} #> entity_antiqs no_check "" @{binding inference} #> diff -r deb9b0283259 -r 998e01d6f8fd src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Doc/more_antiquote.ML Tue Jan 09 15:40:12 2018 +0100 @@ -20,7 +20,7 @@ in val _ = - Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name) + Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name) (fn {context, ...} => class_spec context)); end; @@ -53,7 +53,7 @@ in val _ = - Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term + Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term (fn {context, ...} => pretty_code_thm context)); end; diff -r deb9b0283259 -r 998e01d6f8fd src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Tue Jan 09 15:18:41 2018 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Tue Jan 09 15:40:12 2018 +0100 @@ -104,7 +104,7 @@ Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end in - Thy_Output.antiquotation @{binding "const_typ"} + Document_Antiquotation.setup @{binding "const_typ"} (Scan.lift Args.embedded_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt diff -r deb9b0283259 -r 998e01d6f8fd src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Jan 09 15:40:12 2018 +0100 @@ -983,7 +983,7 @@ end; fun fp_antiquote_setup binding = - Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true}) + Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true}) (fn {source = src, context = ctxt, ...} => fn fcT_name => (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of NONE => error ("Not a known freely generated type name: " ^ quote fcT_name) diff -r deb9b0283259 -r 998e01d6f8fd src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/HOL/Tools/value_command.ML Tue Jan 09 15:40:12 2018 +0100 @@ -73,7 +73,7 @@ >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t))); val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\value\ + (Document_Antiquotation.setup \<^binding>\value\ (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) (fn {source, context, ...} => fn ((name, style), t) => Thy_Output.output context (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/PIDE/resources.ML Tue Jan 09 15:40:12 2018 +0100 @@ -257,13 +257,13 @@ in val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\session\ (Scan.lift (Parse.position Parse.embedded)) + (Document_Antiquotation.setup \<^binding>\session\ (Scan.lift (Parse.position Parse.embedded)) (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #> - Thy_Output.antiquotation \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) + Document_Antiquotation.setup \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_path o #context) #> - Thy_Output.antiquotation \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) + Document_Antiquotation.setup \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_file o #context) #> - Thy_Output.antiquotation \<^binding>\dir\ (Scan.lift (Parse.position Parse.path)) + Document_Antiquotation.setup \<^binding>\dir\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir o #context) #> ML_Antiquotation.value \<^binding>\path\ (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #> diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Pure.thy Tue Jan 09 15:40:12 2018 +0100 @@ -1145,7 +1145,7 @@ Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => - Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of))); + Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/ROOT.ML Tue Jan 09 15:40:12 2018 +0100 @@ -281,6 +281,7 @@ ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; +ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Thy/bibtex.ML Tue Jan 09 15:40:12 2018 +0100 @@ -40,8 +40,8 @@ val _ = Theory.setup - (Thy_Output.add_option \<^binding>\cite_macro\ (Config.put cite_macro) #> - Thy_Output.antiquotation \<^binding>\cite\ + (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro) #> + Document_Antiquotation.setup \<^binding>\cite\ (Scan.lift (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 (Parse.position Args.name))) diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Thy/document_antiquotation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/document_antiquotation.ML Tue Jan 09 15:40:12 2018 +0100 @@ -0,0 +1,184 @@ +(* Title: Pure/Thy/document_antiquotation.ML + Author: Makarius + +Document antiquotations. +*) + +signature DOCUMENT_ANTIQUOTATION = +sig + val thy_output_display: bool Config.T + val thy_output_quotes: bool Config.T + val thy_output_margin: int Config.T + val thy_output_indent: int Config.T + val thy_output_source: bool Config.T + val thy_output_break: bool Config.T + val thy_output_modes: string Config.T + val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context + val print_antiquotations: bool -> Proof.context -> unit + val check: Proof.context -> xstring * Position.T -> string + val check_option: Proof.context -> xstring * Position.T -> string + val setup: binding -> 'a context_parser -> + ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory + val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory + val boolean: string -> bool + val integer: string -> int + val evaluate: Proof.context -> Antiquote.text_antiquote -> string +end; + +structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION = +struct + +(* options *) + +val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>); +val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>); +val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>); +val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>); +val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>); +val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>); +val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>); + + +structure Wrappers = Proof_Data +( + type T = ((unit -> string) -> unit -> string) list; + fun init _ = []; +); + +fun add_wrapper wrapper = Wrappers.map (cons wrapper); + +val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f); + + +(* theory data *) + +structure Data = Theory_Data +( + type T = + (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, + Name_Space.empty_table Markup.document_antiquotation_optionN); + val extend = I; + fun merge ((commands1, options1), (commands2, options2)) : T = + (Name_Space.merge_tables (commands1, commands2), + Name_Space.merge_tables (options1, options2)); +); + +val get_antiquotations = Data.get o Proof_Context.theory_of; + +fun print_antiquotations verbose ctxt = + let + val (commands, options) = get_antiquotations ctxt; + val command_names = map #1 (Name_Space.markup_table verbose ctxt commands); + val option_names = map #1 (Name_Space.markup_table verbose ctxt options); + in + [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), + Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] + end |> Pretty.writeln_chunks; + +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)); +fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)); + +fun setup name scan body thy = + let + fun cmd src ctxt = + let val (x, ctxt') = Token.syntax scan src ctxt + in body {source = src, context = ctxt'} x end; + in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end; + +fun setup_option name opt thy = thy + |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2)); + + +(* syntax *) + +local + +val property = + Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; + +val properties = + Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) []; + +in + +val antiq = + Parse.!!! + (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof) + >> (fn ((name, props), args) => (props, name :: args)); + +end; + + +(* evaluate *) + +local + +fun command src ctxt = + let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src + in f src' ctxt end; + +fun option ((xname, pos), s) ctxt = + let + val (_, opt) = + Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos); + in opt s ctxt end; + +fun eval ctxt (opts, src) = + let + 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 ctxt) (); + val _ = cmd preview_ctxt; + val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN]; + in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; + +in + +fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss + | evaluate ctxt (Antiquote.Control {name, body, ...}) = + eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body])) + | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) = + let val keywords = Thy_Header.get_keywords' ctxt; + in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end; + +end; + + +(* option syntax *) + +fun boolean "" = true + | boolean "true" = true + | boolean "false" = false + | boolean s = error ("Bad boolean value: " ^ quote s); + +fun integer s = + let + fun int ss = + (case Library.read_int ss of (i, []) => i + | _ => error ("Bad integer value: " ^ quote s)); + in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; + +val _ = Theory.setup + (setup_option \<^binding>\show_types\ (Config.put show_types o boolean) #> + setup_option \<^binding>\show_sorts\ (Config.put show_sorts o boolean) #> + setup_option \<^binding>\show_structs\ (Config.put show_structs o boolean) #> + setup_option \<^binding>\show_question_marks\ (Config.put show_question_marks o boolean) #> + setup_option \<^binding>\show_abbrevs\ (Config.put show_abbrevs o boolean) #> + setup_option \<^binding>\names_long\ (Config.put Name_Space.names_long o boolean) #> + setup_option \<^binding>\names_short\ (Config.put Name_Space.names_short o boolean) #> + setup_option \<^binding>\names_unique\ (Config.put Name_Space.names_unique o boolean) #> + setup_option \<^binding>\eta_contract\ (Config.put Syntax_Trans.eta_contract o boolean) #> + setup_option \<^binding>\display\ (Config.put thy_output_display o boolean) #> + setup_option \<^binding>\break\ (Config.put thy_output_break o boolean) #> + setup_option \<^binding>\quotes\ (Config.put thy_output_quotes o boolean) #> + setup_option \<^binding>\mode\ (add_wrapper o Print_Mode.with_modes o single) #> + setup_option \<^binding>\margin\ (Config.put thy_output_margin o integer) #> + setup_option \<^binding>\indent\ (Config.put thy_output_indent o integer) #> + setup_option \<^binding>\source\ (Config.put thy_output_source o boolean) #> + setup_option \<^binding>\goals_limit\ (Config.put Goal_Display.goals_limit o integer)); + +end; diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Tue Jan 09 15:40:12 2018 +0100 @@ -7,12 +7,99 @@ structure Document_Antiquotations: sig end = struct +(* basic entities *) + +local + +fun pretty_term_style ctxt (style, t: term) = + Thy_Output.pretty_term ctxt (style t); + +fun pretty_thm_style ctxt (style, th) = + Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th)); + +fun pretty_term_typ ctxt (style, t: term) = + let val t' = style t + in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; + +fun pretty_term_typeof ctxt (style, t) = + Syntax.pretty_typ ctxt (Term.fastype_of (style t)); + +fun pretty_const ctxt c = + let + val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) + handle TYPE (msg, _, _) => error msg; + val ([t'], _) = Variable.import_terms true [t] ctxt; + in Thy_Output.pretty_term ctxt t' end; + +fun pretty_abbrev ctxt s = + let + val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; + fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); + val (head, args) = Term.strip_comb t; + val (c, T) = Term.dest_Const head handle TERM _ => err (); + val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c + handle TYPE _ => err (); + val t' = Term.betapplys (Envir.expand_atom T (U, u), args); + val eq = Logic.mk_equals (t, t'); + val ctxt' = Variable.auto_fixes eq ctxt; + in Proof_Context.pretty_term_abbrev ctxt' eq end; + +fun pretty_locale ctxt (name, pos) = + let + val thy = Proof_Context.theory_of ctxt + in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end; + +fun pretty_class ctxt = + Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; + +fun pretty_type ctxt s = + let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s + in Pretty.str (Proof_Context.extern_type ctxt name) end; + +fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; + +fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); + +fun basic_entities name scan pretty = + Document_Antiquotation.setup name scan (fn {source, context = ctxt, ...} => + Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source); + +fun basic_entities_style name scan pretty = + Document_Antiquotation.setup name scan + (fn {source, context = ctxt, ...} => fn (style, xs) => + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source + (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs)); + +fun basic_entity name scan = basic_entities name (scan >> single); + +in + +val _ = Theory.setup + (basic_entities_style \<^binding>\thm\ (Term_Style.parse -- Attrib.thms) pretty_thm_style #> + basic_entity \<^binding>\prop\ (Term_Style.parse -- Args.prop) pretty_term_style #> + basic_entity \<^binding>\term\ (Term_Style.parse -- Args.term) pretty_term_style #> + basic_entity \<^binding>\term_type\ (Term_Style.parse -- Args.term) pretty_term_typ #> + basic_entity \<^binding>\typeof\ (Term_Style.parse -- Args.term) pretty_term_typeof #> + basic_entity \<^binding>\const\ (Args.const {proper = true, strict = false}) pretty_const #> + basic_entity \<^binding>\abbrev\ (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> + basic_entity \<^binding>\typ\ Args.typ_abbrev Syntax.pretty_typ #> + basic_entity \<^binding>\locale\ (Scan.lift (Parse.position Args.name)) pretty_locale #> + basic_entity \<^binding>\class\ (Scan.lift Args.embedded_inner_syntax) pretty_class #> + basic_entity \<^binding>\type\ (Scan.lift Args.embedded) pretty_type #> + basic_entities \<^binding>\prf\ Attrib.thms (pretty_prf false) #> + basic_entities \<^binding>\full_prf\ Attrib.thms (pretty_prf true) #> + basic_entity \<^binding>\theory\ (Scan.lift (Parse.position Args.name)) pretty_theory); + +end; + + (* Markdown errors *) local fun markdown_error binding = - Thy_Output.antiquotation binding (Scan.succeed ()) + Document_Antiquotation.setup binding (Scan.succeed ()) (fn {source, ...} => fn _ => error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ Position.here (Position.no_range_position (#1 (Token.range_of source))))) @@ -32,10 +119,14 @@ val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\noindent\ (Scan.succeed ()) (K (K "\\noindent")) #> - Thy_Output.antiquotation \<^binding>\smallskip\ (Scan.succeed ()) (K (K "\\smallskip")) #> - Thy_Output.antiquotation \<^binding>\medskip\ (Scan.succeed ()) (K (K "\\medskip")) #> - Thy_Output.antiquotation \<^binding>\bigskip\ (Scan.succeed ()) (K (K "\\bigskip"))); + (Document_Antiquotation.setup \<^binding>\noindent\ (Scan.succeed ()) + (K (K "\\noindent")) #> + Document_Antiquotation.setup \<^binding>\smallskip\ (Scan.succeed ()) + (K (K "\\smallskip")) #> + Document_Antiquotation.setup \<^binding>\medskip\ (Scan.succeed ()) + (K (K "\\medskip")) #> + Document_Antiquotation.setup \<^binding>\bigskip\ (Scan.succeed ()) + (K (K "\\bigskip"))); (* control style *) @@ -43,7 +134,7 @@ local fun control_antiquotation name s1 s2 = - Thy_Output.antiquotation name (Scan.lift Args.cartouche_input) + Document_Antiquotation.setup name (Scan.lift Args.cartouche_input) (fn {context = ctxt, ...} => enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false}); @@ -63,7 +154,7 @@ local fun text_antiquotation name = - Thy_Output.antiquotation name (Scan.lift Args.text_input) + Document_Antiquotation.setup name (Scan.lift Args.text_input) (fn {context = ctxt, ...} => fn source => (Context_Position.report ctxt (Input.pos_of source) (Markup.language_text (Input.is_delimited source)); @@ -83,7 +174,7 @@ val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\theory_text\ (Scan.lift Args.text_input) + (Document_Antiquotation.setup \<^binding>\theory_text\ (Scan.lift Args.text_input) (fn {context = ctxt, ...} => fn source => let val _ = @@ -93,16 +184,18 @@ val keywords = Thy_Header.get_keywords' ctxt; val toks = Input.source_explode source - |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines + |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ? + Symbol_Pos.trim_lines |> Source.of_list |> Token.source' true keywords |> Source.exhaust; val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); val indentation = - Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space); + Latex.output_symbols + (replicate (Config.get ctxt Document_Antiquotation.thy_output_indent) Symbol.space); in Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |> - (if Config.get ctxt Thy_Output.display then + (if Config.get ctxt Document_Antiquotation.thy_output_display then split_lines #> map (prefix indentation) #> cat_lines #> Latex.environment "isabelle" else enclose "\\isa{" "}") @@ -113,7 +206,7 @@ local -fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ()) +fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ()) (fn {context = ctxt, ...} => fn () => Thy_Output.output ctxt [Goal_Display.pretty_goal @@ -132,7 +225,7 @@ (* embedded lemma *) val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\lemma\ + (Document_Antiquotation.setup \<^binding>\lemma\ (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => @@ -157,7 +250,7 @@ val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\verbatim\ (Scan.lift Args.text_input) + (Document_Antiquotation.setup \<^binding>\verbatim\ (Scan.lift Args.text_input) (fn {context = ctxt, ...} => fn source => (Context_Position.report ctxt (Input.pos_of source) (Markup.language_verbatim (Input.is_delimited source)); @@ -168,7 +261,7 @@ local -fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input) +fun ml_text name ml = Document_Antiquotation.setup name (Scan.lift Args.text_input) (fn {context = ctxt, ...} => fn source => (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source); Thy_Output.verbatim_text ctxt (Input.source_content source))); @@ -198,7 +291,7 @@ (* URLs *) val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\url\ (Scan.lift (Parse.position Parse.embedded)) + (Document_Antiquotation.setup \<^binding>\url\ (Scan.lift (Parse.position Parse.embedded)) (fn {context = ctxt, ...} => fn (name, pos) => (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)]; enclose "\\url{" "}" name))); @@ -207,7 +300,7 @@ (* doc entries *) val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\doc\ (Scan.lift (Parse.position Parse.embedded)) + (Document_Antiquotation.setup \<^binding>\doc\ (Scan.lift (Parse.position Parse.embedded)) (fn {context = ctxt, ...} => fn (name, pos) => (Context_Position.report ctxt pos (Markup.doc name); Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name]))); @@ -216,7 +309,7 @@ (* formal entities *) fun entity_antiquotation name check output = - Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name)) + Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name)) (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name)); val _ = diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Jan 09 15:40:12 2018 +0100 @@ -1,28 +1,11 @@ (* Title: Pure/Thy/thy_output.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Theory document output with antiquotations. +Theory document output. *) signature THY_OUTPUT = sig - val display: bool Config.T - val quotes: bool Config.T - val margin: int Config.T - val indent: int Config.T - val source: bool Config.T - val break: bool Config.T - val modes: string Config.T - val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context - val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory - val check_command: Proof.context -> xstring * Position.T -> string - 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, context: Proof.context} -> 'a -> string) -> theory -> theory - val boolean: string -> bool - val integer: string -> int - 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 @@ -43,152 +26,6 @@ structure Thy_Output: THY_OUTPUT = struct -(** options **) - -val display = Attrib.setup_option_bool ("thy_output_display", \<^here>); -val break = Attrib.setup_option_bool ("thy_output_break", \<^here>); -val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>); -val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>); -val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>); -val source = Attrib.setup_option_bool ("thy_output_source", \<^here>); -val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>); - - -structure Wrappers = Proof_Data -( - type T = ((unit -> string) -> unit -> string) list; - fun init _ = []; -); - -fun add_wrapper wrapper = Wrappers.map (cons wrapper); - -val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f); - - - -(** maintain global antiquotations **) - -structure Antiquotations = Theory_Data -( - type T = - (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, - Name_Space.empty_table Markup.document_antiquotation_optionN); - val extend = I; - fun merge ((commands1, options1), (commands2, options2)) : T = - (Name_Space.merge_tables (commands1, commands2), - Name_Space.merge_tables (options1, options2)); -); - -val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; - -fun add_command name cmd thy = thy - |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd)); - -fun add_option name opt thy = thy - |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd)); - -fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)); - -fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)); - -fun command src ctxt = - let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src - in f src' ctxt end; - -fun option ((xname, pos), s) ctxt = - let - val (_, opt) = - Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos); - in opt s ctxt end; - -fun print_antiquotations verbose ctxt = - let - val (commands, options) = get_antiquotations ctxt; - val command_names = map #1 (Name_Space.markup_table verbose ctxt commands); - val option_names = map #1 (Name_Space.markup_table verbose ctxt options); - in - [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), - Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] - end |> Pretty.writeln_chunks; - -fun antiquotation name scan body = - add_command name - (fn src => fn ctxt => - let val (x, ctxt') = Token.syntax scan src ctxt - in body {source = src, context = ctxt'} x end); - - - -(** syntax of antiquotations **) - -(* option values *) - -fun boolean "" = true - | boolean "true" = true - | boolean "false" = false - | boolean s = error ("Bad boolean value: " ^ quote s); - -fun integer s = - let - fun int ss = - (case Library.read_int ss of (i, []) => i - | _ => error ("Bad integer value: " ^ quote s)); - in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; - - -(* outer syntax *) - -local - -val property = - Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; - -val properties = - Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) []; - -in - -val antiq = - Parse.!!! - (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof) - >> (fn ((name, props), args) => (props, name :: args)); - -end; - - -(* eval antiquote *) - -local - -fun eval_antiq ctxt (opts, src) = - let - 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 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; - -in - -fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss - | 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 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; - - - -(** document output **) - (* output text *) fun output_text ctxt {markdown} source = @@ -199,7 +36,8 @@ val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source)); val output_antiquotes = - map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant]))); + map (fn ant => + Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant]))); fun output_line line = (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ @@ -572,34 +410,12 @@ -(** setup default output **) - -(* options *) - -val _ = Theory.setup - (add_option \<^binding>\show_types\ (Config.put show_types o boolean) #> - add_option \<^binding>\show_sorts\ (Config.put show_sorts o boolean) #> - add_option \<^binding>\show_structs\ (Config.put show_structs o boolean) #> - add_option \<^binding>\show_question_marks\ (Config.put show_question_marks o boolean) #> - add_option \<^binding>\show_abbrevs\ (Config.put show_abbrevs o boolean) #> - add_option \<^binding>\names_long\ (Config.put Name_Space.names_long o boolean) #> - add_option \<^binding>\names_short\ (Config.put Name_Space.names_short o boolean) #> - add_option \<^binding>\names_unique\ (Config.put Name_Space.names_unique o boolean) #> - add_option \<^binding>\eta_contract\ (Config.put Syntax_Trans.eta_contract o boolean) #> - add_option \<^binding>\display\ (Config.put display o boolean) #> - add_option \<^binding>\break\ (Config.put break o boolean) #> - add_option \<^binding>\quotes\ (Config.put quotes o boolean) #> - add_option \<^binding>\mode\ (add_wrapper o Print_Mode.with_modes o single) #> - add_option \<^binding>\margin\ (Config.put margin o integer) #> - add_option \<^binding>\indent\ (Config.put indent o integer) #> - add_option \<^binding>\source\ (Config.put source o boolean) #> - add_option \<^binding>\goals_limit\ (Config.put Goal_Display.goals_limit o integer)); - +(** standard output operations **) (* basic pretty printing *) fun perhaps_trim ctxt = - not (Config.get ctxt display) ? Symbol.trim_blanks; + not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks; fun pretty_text ctxt = Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines; @@ -608,55 +424,6 @@ fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; -fun pretty_term_style ctxt (style, t) = - pretty_term ctxt (style t); - -fun pretty_thm_style ctxt (style, th) = - pretty_term ctxt (style (Thm.full_prop_of th)); - -fun pretty_term_typ ctxt (style, t) = - let val t' = style t - in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; - -fun pretty_term_typeof ctxt (style, t) = - Syntax.pretty_typ ctxt (Term.fastype_of (style t)); - -fun pretty_const ctxt c = - let - val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) - handle TYPE (msg, _, _) => error msg; - val ([t'], _) = Variable.import_terms true [t] ctxt; - in pretty_term ctxt t' end; - -fun pretty_abbrev ctxt s = - let - val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; - fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); - val (head, args) = Term.strip_comb t; - val (c, T) = Term.dest_Const head handle TERM _ => err (); - val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c - handle TYPE _ => err (); - val t' = Term.betapplys (Envir.expand_atom T (U, u), args); - val eq = Logic.mk_equals (t, t'); - val ctxt' = Variable.auto_fixes eq ctxt; - in Proof_Context.pretty_term_abbrev ctxt' eq end; - -fun pretty_locale ctxt (name, pos) = - let - val thy = Proof_Context.theory_of ctxt - in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end; - -fun pretty_class ctxt = - Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; - -fun pretty_type ctxt s = - let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s - in Pretty.str (Proof_Context.extern_type ctxt name) end; - -fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; - -fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); - (* default output *) @@ -664,21 +431,24 @@ fun maybe_pretty_source pretty ctxt src xs = map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) - |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I); + |> (if Config.get ctxt Document_Antiquotation.thy_output_source + then K [pretty_text ctxt (str_of_source src)] else I); -fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin); +fun string_of_margin ctxt = + Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin); fun output ctxt prts = prts - |> Config.get ctxt quotes ? map Pretty.quote - |> (if Config.get ctxt display then - map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output) + |> Config.get ctxt Document_Antiquotation.thy_output_quotes ? map Pretty.quote + |> (if Config.get ctxt Document_Antiquotation.thy_output_display then + map (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) + #> string_of_margin ctxt #> Output.output) #> space_implode "\\isasep\\isanewline%\n" #> Latex.environment "isabelle" else map - ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of) - #> Output.output) + ((if Config.get ctxt Document_Antiquotation.thy_output_break + then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}"); @@ -686,48 +456,14 @@ (* verbatim text *) fun verbatim_text ctxt = - if Config.get ctxt display then - split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #> + if Config.get ctxt Document_Antiquotation.thy_output_display then + split_lines #> + map (prefix (Symbol.spaces (Config.get ctxt Document_Antiquotation.thy_output_indent))) #> + cat_lines #> Latex.output_ascii #> Latex.environment "isabellett" else split_lines #> map (Latex.output_ascii #> enclose "\\isatt{" "}") #> space_implode "\\isasep\\isanewline%\n"; - -(* antiquotations for basic entities *) - -local - -fun basic_entities name scan pretty = - antiquotation name scan (fn {source, context = ctxt, ...} => - output ctxt o maybe_pretty_source pretty ctxt source); - -fun basic_entities_style name scan pretty = - antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) => - output ctxt - (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs)); - -fun basic_entity name scan = basic_entities name (scan >> single); - -in - -val _ = Theory.setup - (basic_entities_style \<^binding>\thm\ (Term_Style.parse -- Attrib.thms) pretty_thm_style #> - basic_entity \<^binding>\prop\ (Term_Style.parse -- Args.prop) pretty_term_style #> - basic_entity \<^binding>\term\ (Term_Style.parse -- Args.term) pretty_term_style #> - basic_entity \<^binding>\term_type\ (Term_Style.parse -- Args.term) pretty_term_typ #> - basic_entity \<^binding>\typeof\ (Term_Style.parse -- Args.term) pretty_term_typeof #> - basic_entity \<^binding>\const\ (Args.const {proper = true, strict = false}) pretty_const #> - basic_entity \<^binding>\abbrev\ (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> - basic_entity \<^binding>\typ\ Args.typ_abbrev Syntax.pretty_typ #> - basic_entity \<^binding>\locale\ (Scan.lift (Parse.position Args.name)) pretty_locale #> - basic_entity \<^binding>\class\ (Scan.lift Args.embedded_inner_syntax) pretty_class #> - basic_entity \<^binding>\type\ (Scan.lift Args.embedded) pretty_type #> - basic_entities \<^binding>\prf\ Attrib.thms (pretty_prf false) #> - basic_entities \<^binding>\full_prf\ Attrib.thms (pretty_prf true) #> - basic_entity \<^binding>\theory\ (Scan.lift (Parse.position Args.name)) pretty_theory); - end; - -end; diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Tools/jedit.ML Tue Jan 09 15:40:12 2018 +0100 @@ -75,7 +75,7 @@ val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\action\ (Scan.lift (Parse.position Parse.embedded)) + (Document_Antiquotation.setup \<^binding>\action\ (Scan.lift (Parse.position Parse.embedded)) (fn {context = ctxt, ...} => fn (name, pos) => (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else (); Thy_Output.verbatim_text ctxt name))); diff -r deb9b0283259 -r 998e01d6f8fd src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Pure/Tools/rail.ML Tue Jan 09 15:40:12 2018 +0100 @@ -332,7 +332,7 @@ fun output_rules ctxt rules = let - val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq; + val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq; fun output_text b s = Output.output s |> b ? enclose "\\isakeyword{" "}" @@ -374,7 +374,7 @@ in Latex.environment "railoutput" (implode (map output_rule rules)) end; val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\rail\ (Scan.lift Args.text_input) + (Document_Antiquotation.setup \<^binding>\rail\ (Scan.lift Args.text_input) (fn {context = ctxt, ...} => output_rules ctxt o read ctxt)); end; diff -r deb9b0283259 -r 998e01d6f8fd src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Jan 09 15:18:41 2018 +0100 +++ b/src/Tools/Code/code_target.ML Tue Jan 09 15:40:12 2018 +0100 @@ -510,7 +510,7 @@ in val _ = Theory.setup - (Thy_Output.antiquotation @{binding code_stmts} + (Document_Antiquotation.setup @{binding code_stmts} (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))