--- 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))
\<close>
setup \<open>
Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ
- (fn ctxt => fn T => [Syntax.pretty_typ ctxt T])
+ Syntax.pretty_typ
\<close>
(*>*)
text\<open>
--- 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>\<open>const_typ\<close> (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)
\<close>
--- 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;
--- 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>\<open>const_typ\<close> (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)
\<close>
--- 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;
--- 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>\<open>value\<close>
(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>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
--- 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>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
- basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
+ (basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
@@ -85,9 +82,12 @@
basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory #>
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
- basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
+ Document_Antiquotation.setup \<^binding>\<open>thm\<close> (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 *)
--- 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 *)