new antiquotation const_typ
authornipkow
Fri Sep 28 08:39:48 2012 +0200 (2012-09-28)
changeset 496288262d35eff20
parent 49627 34ada66545ca
child 49629 99700c4e0b33
new antiquotation const_typ
src/Doc/LaTeXsugar/Sugar.thy
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:09:28 2012 +0200
     1.2 +++ b/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:39:48 2012 +0200
     1.3 @@ -525,6 +525,16 @@
     1.4  \end{quote}
     1.5  The \texttt{isabelle} environment is the one defined in the standard file
     1.6  \texttt{isabelle.sty} which most likely you are loading anyway.
     1.7 +
     1.8 +
     1.9 +\section{Antiquotation}
    1.10 +
    1.11 +You want to show a constant and its type? Instead of going
    1.12 +\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
    1.13 +you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
    1.14 +\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
    1.15 +\verb!@!\verb!{const_typ length}! produces @{const_typ length}.
    1.16 +
    1.17  *}
    1.18  
    1.19  (*<*)
     2.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:09:28 2012 +0200
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:39:48 2012 +0200
     2.3 @@ -97,5 +97,21 @@
     2.4    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
     2.5    "_asm" :: "prop \<Rightarrow> asms" ("_")
     2.6  
     2.7 +setup{*
     2.8 +  let
     2.9 +    fun pretty ctxt c =
    2.10 +      let val tc = Proof_Context.read_const_proper ctxt false c
    2.11 +      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    2.12 +            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    2.13 +      end
    2.14 +  in
    2.15 +    Thy_Output.antiquotation @{binding "const_typ"}
    2.16 +     (Scan.lift Args.name_source)
    2.17 +       (fn {source = src, context = ctxt, ...} => fn arg =>
    2.18 +          Thy_Output.output ctxt
    2.19 +            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    2.20 +  end;
    2.21 +*}
    2.22 +
    2.23  end
    2.24  (*>*)
    2.25 \ No newline at end of file