# HG changeset patch # User wenzelm # Date 1516308090 -3600 # Node ID a5ca98950a914a0a28bee524c9770c7a71ac5a03 # Parent c23d9375e66118ec6417892e7a9d74726192604f clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification; diff -r c23d9375e661 -r a5ca98950a91 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Doc/Main/Main_Doc.thy Thu Jan 18 21:41:30 2018 +0100 @@ -4,23 +4,15 @@ begin setup \ - let - fun pretty_term_type_only ctxt (t, T) = + Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev) + (fn ctxt => fn (t, T) => (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () else error "term_type_only: type mismatch"; - Syntax.pretty_typ ctxt T) - in - Document_Antiquotation.setup @{binding term_type_only} - (Args.term -- Args.typ_abbrev) - (fn {source, context = ctxt, ...} => fn arg => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) - end + [Syntax.pretty_typ ctxt T])) \ setup \ - 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) + Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ + (fn ctxt => fn T => [Syntax.pretty_typ ctxt T]) \ (*>*) text\ diff -r c23d9375e661 -r a5ca98950a91 src/Doc/Prog_Prove/LaTeXsugar.thy --- a/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Jan 18 21:41:30 2018 +0100 @@ -43,20 +43,13 @@ "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") -setup\ - let - fun pretty ctxt c = - let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c - in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", - Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] - end - in - Document_Antiquotation.setup @{binding "const_typ"} - (Scan.lift Args.embedded_inner_syntax) - (fn {source = src, context = ctxt, ...} => fn arg => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source pretty ctxt src [arg])) - end; +setup \ + Thy_Output.antiquotation_pretty_source \<^binding>\const_typ\ (Scan.lift Args.embedded_inner_syntax) + (fn ctxt => fn c => + let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in + [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]] + end) \ end diff -r c23d9375e661 -r a5ca98950a91 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Doc/antiquote_setup.ML Thu Jan 18 21:41:30 2018 +0100 @@ -73,9 +73,9 @@ fun prep_ml source = (Input.source_content source, ML_Lex.read_source false source); -fun index_ml name kind ml = Document_Antiquotation.setup name +fun index_ml name kind ml = Thy_Output.antiquotation_raw name (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input))) - (fn {context = ctxt, ...} => fn (source1, opt_source2) => + (fn ctxt => fn (source1, opt_source2) => let val (txt1, toks1) = prep_ml source1; val (txt2, toks2) = @@ -98,8 +98,9 @@ handle ERROR msg => error (msg ^ Position.here pos); val kind' = if kind = "" then "ML" else "ML " ^ kind; in - "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ - (Thy_Output.verbatim_text ctxt txt') + Latex.block + [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"), + Thy_Output.verbatim ctxt txt'] end); in @@ -119,29 +120,18 @@ (* named theorems *) val _ = - Theory.setup (Document_Antiquotation.setup @{binding named_thms} + Theory.setup (Thy_Output.antiquotation_raw @{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 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 Document_Antiquotation.thy_output_indent) p)) ^ - "\\rulename{" ^ - Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}") - #> space_implode "\\par\\smallskip%\n" - #> Latex.environment "isabelle" - else - map (fn (p, name) => - Output.output (Pretty.unformatted_string_of p) ^ - "\\rulename{" ^ - Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}") - #> space_implode "\\par\\smallskip%\n" - #> enclose "\\isa{" "}"))); + (fn ctxt => + map (fn (thm, name) => + Output.output + (Document_Antiquotation.format ctxt + (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^ + enclose "\\rulename{" "}" + (Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)))) + #> space_implode "\\par\\smallskip%\n" + #> Latex.string #> single + #> Thy_Output.isabelle ctxt)); (* Isabelle/Isar entities (with index) *) @@ -161,11 +151,11 @@ val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = - Document_Antiquotation.setup + Thy_Output.antiquotation_raw (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)) - (fn {context = ctxt, ...} => fn (logic, (name, pos)) => + (fn ctxt => fn (logic, (name, pos)) => let val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); val hyper_name = @@ -180,12 +170,12 @@ "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); val _ = if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); - in - idx ^ - (Output.output name - |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") - |> hyper o enclose "\\mbox{\\isa{" "}}") - end); + val latex = + idx ^ + (Output.output name + |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") + |> hyper o enclose "\\mbox{\\isa{" "}}"); + in Latex.string latex end); fun entity_antiqs check markup kind = entity check markup kind NONE #> diff -r c23d9375e661 -r a5ca98950a91 src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Doc/more_antiquote.ML Thu Jan 18 21:41:30 2018 +0100 @@ -9,53 +9,37 @@ (* class specifications *) -local - -fun class_spec ctxt s = - let - val thy = Proof_Context.theory_of ctxt; - val class = Sign.intern_class thy s; - in Thy_Output.output ctxt (Class.pretty_specification thy class) end; - -in - val _ = - Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name) - (fn {context, ...} => class_spec context)); - -end; + Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name) + (fn ctxt => fn s => + let + val thy = Proof_Context.theory_of ctxt; + val class = Sign.intern_class thy s; + in Class.pretty_specification thy class end)); (* code theorem antiquotation *) -local - fun no_vars ctxt thm = let val ctxt' = Variable.set_body false ctxt; val ((_, [thm]), _) = Variable.import true [thm] ctxt'; in thm end; -fun pretty_code_thm ctxt raw_const = - let - val thy = Proof_Context.theory_of ctxt; - val const = Code.check_const thy raw_const; - val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] }; - fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; - val thms = Code_Preproc.cert eqngr const - |> Code.equations_of_cert thy - |> snd - |> these - |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) - |> map (holize o no_vars ctxt o Axclass.overload ctxt); - in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end; - -in - val _ = - Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term - (fn {context, ...} => pretty_code_thm context)); + Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term + (fn ctxt => fn raw_const => + let + val thy = Proof_Context.theory_of ctxt; + val const = Code.check_const thy raw_const; + val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] }; + fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; + val thms = Code_Preproc.cert eqngr const + |> Code.equations_of_cert thy + |> snd + |> these + |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) + |> map (holize o no_vars ctxt o Axclass.overload ctxt); + in map (Thy_Output.pretty_thm ctxt) thms end)); end; - -end; diff -r c23d9375e661 -r a5ca98950a91 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 18 21:29:28 2018 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Thu Jan 18 21:41:30 2018 +0100 @@ -96,20 +96,13 @@ "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") -setup\ - let - fun pretty ctxt c = - let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c - in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", - Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] - end - in - Document_Antiquotation.setup @{binding "const_typ"} - (Scan.lift Args.embedded_inner_syntax) - (fn {source = src, context = ctxt, ...} => fn arg => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source pretty ctxt src [arg])) - end; +setup \ + Thy_Output.antiquotation_pretty_source \<^binding>\const_typ\ (Scan.lift Args.embedded_inner_syntax) + (fn ctxt => fn c => + let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in + [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]] + end) \ setup\ diff -r c23d9375e661 -r a5ca98950a91 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 18 21:41:30 2018 +0100 @@ -983,8 +983,8 @@ end; fun fp_antiquote_setup binding = - Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true}) - (fn {source = src, context = ctxt, ...} => fn fcT_name => + Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true}) + (fn 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) | SOME {T = T0, ctrs = ctrs0, ...} => @@ -1002,9 +1002,6 @@ Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 :: Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 :: flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs))); - in - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()]) - end)); + in [pretty_co_datatype] end)); end; diff -r c23d9375e661 -r a5ca98950a91 src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/HOL/Tools/value_command.ML Thu Jan 18 21:41:30 2018 +0100 @@ -73,11 +73,10 @@ >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t))); val _ = Theory.setup - (Document_Antiquotation.setup \<^binding>\value\ + (Thy_Output.antiquotation_pretty_source \<^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 - [style (value_select name context t)])) + (fn ctxt => fn ((name, style), t) => + [Thy_Output.pretty_term ctxt (style (value_select name ctxt t))]) #> add_evaluator (\<^binding>\simp\, Code_Simp.dynamic_value) #> snd #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd #> add_evaluator (\<^binding>\code\, Code_Evaluation.dynamic_value_strict) #> snd); diff -r c23d9375e661 -r a5ca98950a91 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/PIDE/resources.ML Thu Jan 18 21:41:30 2018 +0100 @@ -243,12 +243,11 @@ let val dir = master_directory (Proof_Context.theory_of ctxt); val _ = check ctxt dir (name, pos); - in - space_explode "/" name - |> map Latex.output_ascii - |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}") - |> enclose "\\isatt{" "}" - end; + val latex = + space_explode "/" name + |> map Latex.output_ascii + |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}"); + in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end; fun ML_antiq check ctxt (name, pos) = let val path = check ctxt Path.current (name, pos); @@ -257,14 +256,14 @@ in val _ = Theory.setup - (Document_Antiquotation.setup \<^binding>\session\ (Scan.lift (Parse.position Parse.embedded)) - (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #> - Document_Antiquotation.setup \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) - (document_antiq check_path o #context) #> - Document_Antiquotation.setup \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) - (document_antiq check_file o #context) #> - Document_Antiquotation.setup \<^binding>\dir\ (Scan.lift (Parse.position Parse.path)) - (document_antiq check_dir o #context) #> + (Thy_Output.antiquotation_verbatim \<^binding>\session\ + (Scan.lift (Parse.position Parse.embedded)) check_session #> + Thy_Output.antiquotation_raw \<^binding>\path\ + (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #> + Thy_Output.antiquotation_raw \<^binding>\file\ + (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #> + Thy_Output.antiquotation_raw \<^binding>\dir\ + (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #> ML_Antiquotation.value \<^binding>\path\ (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #> ML_Antiquotation.value \<^binding>\file\ diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Thy/bibtex.ML Thu Jan 18 21:41:30 2018 +0100 @@ -41,11 +41,11 @@ val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro) #> - Document_Antiquotation.setup \<^binding>\cite\ + Thy_Output.antiquotation_raw \<^binding>\cite\ (Scan.lift (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 (Parse.position Args.name))) - (fn {context = ctxt, ...} => fn (opt, citations) => + (fn ctxt => fn (opt, citations) => let val thy = Proof_Context.theory_of ctxt; val bibtex_entries = Present.get_bibtex_entries thy; @@ -60,6 +60,6 @@ (map (fn (name, pos) => (pos, Markup.citation name)) citations); val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]"); val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; - in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end)); + in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end)); end; diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Thy/document_antiquotation.ML --- a/src/Pure/Thy/document_antiquotation.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Thy/document_antiquotation.ML Thu Jan 18 21:41:30 2018 +0100 @@ -13,15 +13,22 @@ val thy_output_source: bool Config.T val thy_output_break: bool Config.T val thy_output_modes: string Config.T + val trim_blanks: Proof.context -> string -> string + val trim_lines: Proof.context -> string -> string + val indent_lines: Proof.context -> string -> string + val quote: Proof.context -> Pretty.T -> Pretty.T + val indent: Proof.context -> Pretty.T -> Pretty.T + val format: Proof.context -> Pretty.T -> string + val output: Proof.context -> Pretty.T -> Output.output 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 + ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> 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 + val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list end; structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION = @@ -38,12 +45,44 @@ val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>); +(* blanks *) + +fun trim_blanks ctxt = + not (Config.get ctxt thy_output_display) ? Symbol.trim_blanks; + +fun trim_lines ctxt = + if not (Config.get ctxt thy_output_display) then + split_lines #> map Symbol.trim_blanks #> space_implode " " + else I; + +fun indent_lines ctxt = + if Config.get ctxt thy_output_display then + prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent)) + else I; + + +(* output *) + +fun quote ctxt = + Config.get ctxt thy_output_quotes ? Pretty.quote; + +fun indent ctxt = + Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent); + +fun format ctxt = + if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break + then Pretty.string_of_margin (Config.get ctxt thy_output_margin) + else Pretty.unformatted_string_of; + +fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output; + + (* theory data *) structure Data = Theory_Data ( type T = - (Token.src -> Proof.context -> string) Name_Space.table * + (Token.src -> Proof.context -> Latex.text) Name_Space.table * (string -> Proof.context -> Proof.context) Name_Space.table; val empty : T = (Name_Space.empty_table Markup.document_antiquotationN, @@ -73,7 +112,7 @@ let fun cmd src ctxt = let val (x, ctxt') = Token.syntax scan src ctxt - in body {source = src, context = ctxt'} x end; + in body {context = ctxt', source = src, argument = 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 @@ -119,11 +158,11 @@ val preview_ctxt = fold option opts ctxt; val print_ctxt = Context_Position.set_visible false preview_ctxt; val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN]; - in Print_Mode.with_modes print_modes (fn () => command src print_ctxt) () end; + in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end; in -fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss +fun evaluate _ (Antiquote.Text ss) = [Latex.symbols 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, ...}) = @@ -138,13 +177,13 @@ fun boolean "" = true | boolean "true" = true | boolean "false" = false - | boolean s = error ("Bad boolean value: " ^ quote s); + | boolean s = error ("Bad boolean value: " ^ Library.quote s); fun integer s = let fun int ss = (case Library.read_int ss of (i, []) => i - | _ => error ("Bad integer value: " ^ quote s)); + | _ => error ("Bad integer value: " ^ Library.quote s)); in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; val _ = Theory.setup diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Thu Jan 18 21:41:30 2018 +0100 @@ -11,17 +11,19 @@ local -fun pretty_term_style ctxt (style, t: term) = +type style = term -> term; + +fun pretty_term_style ctxt (style: style, t) = Thy_Output.pretty_term ctxt (style t); -fun pretty_thm_style ctxt (style, th) = +fun pretty_thm_style ctxt (style: style, th) = Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th)); -fun pretty_term_typ ctxt (style, t: term) = +fun pretty_term_typ ctxt (style: style, t) = 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) = +fun pretty_term_typeof ctxt (style: style, t) = Syntax.pretty_typ ctxt (Term.fastype_of (style t)); fun pretty_const ctxt c = @@ -61,15 +63,11 @@ 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); + Thy_Output.antiquotation_pretty_source name scan (map o pretty); 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)); + Thy_Output.antiquotation_pretty_source name scan + (fn ctxt => fn (style: style, xs) => map (fn x => pretty ctxt (style, x)) xs); fun basic_entity name scan = basic_entities name (scan >> single); @@ -100,9 +98,9 @@ fun markdown_error binding = Document_Antiquotation.setup binding (Scan.succeed ()) - (fn {source, ...} => fn _ => + (fn {source = src, ...} => error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ - Position.here (Position.no_range_position (#1 (Token.range_of source))))) + Position.here (Position.no_range_position (#1 (Token.range_of src))))) in @@ -119,14 +117,14 @@ val _ = Theory.setup - (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"))); + (Thy_Output.antiquotation_raw \<^binding>\noindent\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\noindent") #> + Thy_Output.antiquotation_raw \<^binding>\smallskip\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\smallskip") #> + Thy_Output.antiquotation_raw \<^binding>\medskip\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\medskip") #> + Thy_Output.antiquotation_raw \<^binding>\bigskip\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\bigskip")); (* control style *) @@ -134,9 +132,8 @@ local fun control_antiquotation name s1 s2 = - 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}); + Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input) + (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_text ctxt {markdown = false}); in @@ -154,11 +151,13 @@ local fun text_antiquotation name = - 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)); - Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)])); + Thy_Output.antiquotation_raw name (Scan.lift Args.text_input) + (fn ctxt => fn text => + let + val _ = + Context_Position.report ctxt (Input.pos_of text) + (Markup.language_text (Input.is_delimited text)); + in Thy_Output.pretty ctxt [Thy_Output.pretty_text ctxt (Input.source_content text)] end); in @@ -174,41 +173,37 @@ val _ = Theory.setup - (Document_Antiquotation.setup \<^binding>\theory_text\ (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => fn source => + (Thy_Output.antiquotation_raw \<^binding>\theory_text\ (Scan.lift Args.text_input) + (fn ctxt => fn text => let + val keywords = Thy_Header.get_keywords' ctxt; + val _ = - Context_Position.report ctxt (Input.pos_of source) - (Markup.language_Isar (Input.is_delimited source)); - - val keywords = Thy_Header.get_keywords' ctxt; - val toks = - Input.source_explode source - |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ? - Symbol_Pos.trim_lines + Context_Position.report ctxt (Input.pos_of text) + (Markup.language_Isar (Input.is_delimited text)); + val _ = + Input.source_explode text |> 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 Document_Antiquotation.thy_output_indent) Symbol.space); - in - Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |> - (if Config.get ctxt Document_Antiquotation.thy_output_display then - split_lines #> map (prefix indentation) #> cat_lines #> - Latex.environment "isabelle" - else enclose "\\isa{" "}") - end)); + |> Source.exhaust + |> maps (Token.reports keywords) + |> Context_Position.reports_text ctxt; + + val toks = + Input.source_content text + |> Document_Antiquotation.trim_lines ctxt + |> Document_Antiquotation.indent_lines ctxt + |> Token.explode keywords Position.none; + in Thy_Output.isabelle ctxt (maps (Thy_Output.output_token ctxt) toks) end)); (* goal state *) local -fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ()) - (fn {context = ctxt, ...} => fn () => - Thy_Output.output ctxt +fun goal_state name main = + Thy_Output.antiquotation_pretty name (Scan.succeed ()) + (fn ctxt => fn () => [Goal_Display.pretty_goal (Config.put Goal_Display.show_main_goal main ctxt) (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]); @@ -228,7 +223,7 @@ (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)) => + (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => let val reports = (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: @@ -239,32 +234,30 @@ val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof (m1, m2); - in - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source - Thy_Output.pretty_term ctxt [hd source, prop_token] [prop]) - end)); + in Thy_Output.pretty_source ctxt [hd src, prop_tok] [Thy_Output.pretty_term ctxt prop] end)); (* verbatim text *) -val _ = - Theory.setup - (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)); - Thy_Output.verbatim_text ctxt (Input.source_content source)))); +val _ = Theory.setup + (Thy_Output.antiquotation_verbatim \<^binding>\verbatim\ (Scan.lift Args.text_input) + (fn ctxt => fn text => + let + val _ = + Context_Position.report ctxt (Input.pos_of text) + (Markup.language_verbatim (Input.is_delimited text)); + in Input.source_content text end)); (* ML text *) local -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))); +fun ml_text name ml = + Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input) + (fn ctxt => fn text => + let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text) + in Input.source_content text end); fun ml_enclose bg en source = ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en; @@ -291,34 +284,39 @@ (* URLs *) val _ = Theory.setup - (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))); + (Thy_Output.antiquotation_raw \<^binding>\url\ (Scan.lift (Parse.position Parse.embedded)) + (fn ctxt => fn (url, pos) => + let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)] + in Latex.enclose_block "\\url{" "}" [Latex.string url] end)); (* doc entries *) val _ = Theory.setup - (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]))); + (Thy_Output.antiquotation_pretty \<^binding>\doc\ (Scan.lift (Parse.position Parse.embedded)) + (fn ctxt => fn (name, pos) => + let val _ = Context_Position.report ctxt pos (Markup.doc name) + in [Thy_Output.pretty_text ctxt name] end)); (* formal entities *) -fun entity_antiquotation name check output = - Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name)) - (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name)); +local + +fun entity_antiquotation name check bg en = + Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name)) + (fn ctxt => fn (name, pos) => + let val _ = check ctxt (name, pos) + in Latex.enclose_block bg en [Latex.string (Output.output name)] end); + +in val _ = Theory.setup - (entity_antiquotation \<^binding>\command\ Outer_Syntax.check_command - (enclose "\\isacommand{" "}" o Output.output) #> - entity_antiquotation \<^binding>\method\ Method.check_name - (enclose "\\isa{" "}" o Output.output) #> - entity_antiquotation \<^binding>\attribute\ Attrib.check_name - (enclose "\\isa{" "}" o Output.output)); + (entity_antiquotation \<^binding>\command\ Outer_Syntax.check_command "\\isacommand{" "}" #> + entity_antiquotation \<^binding>\method\ Method.check_name "\\isa{" "}" #> + entity_antiquotation \<^binding>\attribute\ Attrib.check_name "\\isa{" "}"); end; + +end; diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Jan 18 21:41:30 2018 +0100 @@ -15,12 +15,21 @@ val pretty_text: Proof.context -> string -> Pretty.T val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T - val str_of_source: Token.src -> string - val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context -> - Token.src -> 'a list -> Pretty.T list - 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 lines: Latex.text list -> Latex.text list + val isabelle: Proof.context -> Latex.text list -> Latex.text + val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text + val typewriter: Proof.context -> string -> Latex.text + val verbatim: Proof.context -> string -> Latex.text + val pretty: Proof.context -> Pretty.T list -> Latex.text + val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text + val antiquotation_pretty: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory + val antiquotation_pretty_source: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory + val antiquotation_raw: + binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory + val antiquotation_verbatim: + binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory end; structure Thy_Output: THY_OUTPUT = @@ -35,9 +44,7 @@ val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source)); - val output_antiquotes = - map (fn ant => - Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant]))); + val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt); fun output_line line = (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ @@ -60,7 +67,7 @@ in output_blocks blocks end else let - val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); + val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); val reports = Antiquote.antiq_reports ants; val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants); in output_antiquotes ants end @@ -421,58 +428,63 @@ (** standard output operations **) -(* basic pretty printing *) - -fun perhaps_trim ctxt = - not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks; +(* pretty printing *) fun pretty_text ctxt = - Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines; + Pretty.chunks o map (Pretty.str o Document_Antiquotation.trim_blanks ctxt) o split_lines; -fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; +fun pretty_term ctxt t = + Syntax.pretty_term (Variable.auto_fixes t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; (* default output *) -val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src; +val lines = separate (Latex.string "\\isasep\\isanewline%\n"); -fun maybe_pretty_source pretty ctxt src xs = - map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) - |> (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 Document_Antiquotation.thy_output_margin); +fun isabelle ctxt body = + if Config.get ctxt Document_Antiquotation.thy_output_display + then Latex.environment_block "isabelle" body + else Latex.block (Latex.enclose_body "\\isa{" "}" body); -fun output ctxt prts = - prts - |> 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 Document_Antiquotation.thy_output_break - then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output) - #> space_implode "\\isasep\\isanewline%\n" - #> enclose "\\isa{" "}"); +fun isabelle_typewriter ctxt body = + if Config.get ctxt Document_Antiquotation.thy_output_display + then Latex.environment_block "isabellett" body + else Latex.block (Latex.enclose_body "\\isatt{" "}" body); + +fun typewriter ctxt s = + isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)]; + +fun verbatim ctxt = + if Config.get ctxt Document_Antiquotation.thy_output_display + then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt + else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; -(* verbatim text *) +(* pretty output *) + +fun pretty ctxt = + map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt; + +fun pretty_source ctxt src prts = + if Config.get ctxt Document_Antiquotation.thy_output_source then + pretty ctxt [pretty_text ctxt (space_implode " " (map Token.unparse (Token.args_of_src src)))] + else pretty ctxt prts; -fun verbatim_text ctxt = - 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"; +fun antiquotation_pretty name scan f = + Document_Antiquotation.setup name scan + (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x)); + +fun antiquotation_pretty_source name scan f = + Document_Antiquotation.setup name scan + (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x)); + +fun antiquotation_raw name scan f = + Document_Antiquotation.setup name scan + (fn {context = ctxt, argument = x, ...} => f ctxt x); + +fun antiquotation_verbatim name scan f = + antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt); end; diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Tools/jedit.ML Thu Jan 18 21:41:30 2018 +0100 @@ -75,10 +75,14 @@ val _ = Theory.setup - (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))); + (Thy_Output.antiquotation_verbatim \<^binding>\action\ (Scan.lift (Parse.position Parse.embedded)) + (fn ctxt => fn (name, pos) => + let + val _ = + if Context_Position.is_reported ctxt pos + then ignore (check_action (name, pos)) + else (); + in name end)); end; diff -r c23d9375e661 -r a5ca98950a91 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Pure/Tools/rail.ML Thu Jan 18 21:41:30 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: Proof.context -> (string Antiquote.antiquote * rail) list -> string + val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text end; structure Rail: RAIL = @@ -339,7 +339,8 @@ fun output_rules ctxt rules = let - val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq; + val output_antiq = + Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq; fun output_text b s = Output.output s |> b ? enclose "\\isakeyword{" "}" @@ -378,11 +379,11 @@ output "" rail' ^ "\\rail@end\n" end; - in Latex.environment "railoutput" (implode (map output_rule rules)) end; + in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end; val _ = Theory.setup - (Document_Antiquotation.setup \<^binding>\rail\ (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => output_rules ctxt o read ctxt)); + (Thy_Output.antiquotation_raw \<^binding>\rail\ (Scan.lift Args.text_input) + (fn ctxt => output_rules ctxt o read ctxt)); end; diff -r c23d9375e661 -r a5ca98950a91 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Jan 18 21:29:28 2018 +0100 +++ b/src/Tools/Code/code_target.ML Thu Jan 18 21:41:30 2018 +0100 @@ -510,14 +510,15 @@ in val _ = Theory.setup - (Document_Antiquotation.setup @{binding code_stmts} + (Thy_Output.antiquotation_raw @{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))) - (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) => - present_code ctxt (mk_cs ctxt) + (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) => + Latex.string + (present_code ctxt (mk_cs ctxt) (maps (fn f => f ctxt) mk_stmtss) - target_name some_width "Example" [])); + target_name some_width "Example" []))); end;