# HG changeset patch # User wenzelm # Date 1516886035 -3600 # Node ID ceb324e34c149b36266022068b92c9029b920eb0 # Parent 310114bec0d78e311eed1f33bcdb2f8fb19b4e18 clarified signature: items with \isasep are special; diff -r 310114bec0d7 -r ceb324e34c14 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Thu Jan 25 11:29:52 2018 +0100 +++ b/src/Doc/Main/Main_Doc.thy Thu Jan 25 14:13:55 2018 +0100 @@ -8,11 +8,11 @@ (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])) + Syntax.pretty_typ ctxt T)) \ setup \ Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ - (fn ctxt => fn T => [Syntax.pretty_typ ctxt T]) + Syntax.pretty_typ \ (*>*) text\ diff -r 310114bec0d7 -r ceb324e34c14 src/Doc/Prog_Prove/LaTeXsugar.thy --- a/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Jan 25 11:29:52 2018 +0100 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Jan 25 14:13:55 2018 +0100 @@ -47,8 +47,8 @@ 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)]] + Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end) \ diff -r 310114bec0d7 -r ceb324e34c14 src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Thu Jan 25 11:29:52 2018 +0100 +++ b/src/Doc/more_antiquote.ML Thu Jan 25 14:13:55 2018 +0100 @@ -15,7 +15,7 @@ let val thy = Proof_Context.theory_of ctxt; val class = Sign.intern_class thy s; - in Class.pretty_specification thy class end)); + in Pretty.chunks (Class.pretty_specification thy class) end)); (* code theorem antiquotation *) @@ -40,6 +40,6 @@ |> 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)); + in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end)); end; diff -r 310114bec0d7 -r ceb324e34c14 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 25 11:29:52 2018 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Thu Jan 25 14:13:55 2018 +0100 @@ -100,8 +100,8 @@ 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)]] + Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end) \ diff -r 310114bec0d7 -r ceb324e34c14 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 25 11:29:52 2018 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 25 14:13:55 2018 +0100 @@ -998,10 +998,10 @@ fun pretty_ctr ctr = Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr :: map pretty_typ_bracket (binder_types (fastype_of ctr)))); - val pretty_co_datatype = - 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 [pretty_co_datatype] end)); + in + 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))) + end)); end; diff -r 310114bec0d7 -r ceb324e34c14 src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML Thu Jan 25 11:29:52 2018 +0100 +++ b/src/HOL/Tools/value_command.ML Thu Jan 25 14:13:55 2018 +0100 @@ -76,7 +76,7 @@ (Thy_Output.antiquotation_pretty_source \<^binding>\value\ (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) (fn ctxt => fn ((name, style), t) => - [Thy_Output.pretty_term ctxt (style (value_select name ctxt 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 310114bec0d7 -r ceb324e34c14 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Jan 25 11:29:52 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Thu Jan 25 14:13:55 2018 +0100 @@ -16,8 +16,8 @@ fun pretty_term_style ctxt (style: style, t) = Thy_Output.pretty_term ctxt (style t); -fun pretty_thm_style ctxt (style: style, th) = - Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th)); +fun pretty_thms_style ctxt (style: style, ths) = + map (fn th => Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths; fun pretty_term_typ ctxt (style: style, t) = let val t' = style t @@ -62,20 +62,17 @@ fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); -fun basic_entities name scan pretty = - Thy_Output.antiquotation_pretty_source name scan (map o pretty); +val basic_entity = Thy_Output.antiquotation_pretty_source; -fun basic_entities_style name scan pretty = - 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); +fun basic_entities name scan pretty = + Document_Antiquotation.setup name scan + (fn {context = ctxt, source = src, argument = xs} => + Thy_Output.pretty_items_source ctxt src (map (pretty ctxt) xs)); 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>\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 #> @@ -85,9 +82,12 @@ 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_entity \<^binding>\theory\ (Scan.lift (Parse.position Args.name)) pretty_theory #> 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); + Document_Antiquotation.setup \<^binding>\thm\ (Term_Style.parse -- Attrib.thms) + (fn {context = ctxt, source = src, argument = arg} => + Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg))); end; @@ -207,9 +207,9 @@ fun goal_state name main = Thy_Output.antiquotation_pretty name (Scan.succeed ()) (fn ctxt => fn () => - [Goal_Display.pretty_goal + Goal_Display.pretty_goal (Config.put Goal_Display.show_main_goal main ctxt) - (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))]); + (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))); in @@ -237,7 +237,7 @@ val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof (m1, m2); - in Thy_Output.pretty_source ctxt [hd src, prop_tok] [Thy_Output.pretty_term ctxt prop] end)); + in Thy_Output.pretty_source ctxt [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop) end)); (* verbatim text *) diff -r 310114bec0d7 -r ceb324e34c14 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Jan 25 11:29:52 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Jan 25 14:13:55 2018 +0100 @@ -15,18 +15,20 @@ Token.T list -> Latex.text list val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T - val lines: Latex.text list -> Latex.text list + val items: 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 source: Proof.context -> Token.src -> Latex.text - val pretty: Proof.context -> Pretty.T list -> Latex.text - val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text + val pretty: Proof.context -> Pretty.T -> Latex.text + val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text + val pretty_items: Proof.context -> Pretty.T list -> Latex.text + val pretty_items_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 + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_source: - binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_raw: binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory val antiquotation_verbatim: @@ -444,7 +446,7 @@ (* default output *) -val lines = separate (Latex.string "\\isasep\\isanewline%\n"); +val items = separate (Latex.string "\\isasep\\isanewline%\n"); fun isabelle ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display @@ -462,7 +464,7 @@ 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; + else split_lines #> map (typewriter ctxt) #> items #> Latex.block; fun source ctxt = Token.args_of_src @@ -472,11 +474,18 @@ #> isabelle ctxt; fun pretty ctxt = - map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt; + Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt; + +fun pretty_source ctxt src prt = + if Config.get ctxt Document_Antiquotation.thy_output_source + then source ctxt src else pretty ctxt prt; -fun pretty_source ctxt src prts = +fun pretty_items ctxt = + map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt; + +fun pretty_items_source ctxt src prts = if Config.get ctxt Document_Antiquotation.thy_output_source - then source ctxt src else pretty ctxt prts; + then source ctxt src else pretty_items ctxt prts; (* antiquotation variants *)