# HG changeset patch
# User nipkow
# Date 1348814388 -7200
# Node ID 8262d35eff20accabc66771a7351565ea6ee4e71
# Parent  34ada66545ca27885897b7edaef165f62751f18a
new antiquotation const_typ

diff -r 34ada66545ca -r 8262d35eff20 src/Doc/LaTeXsugar/Sugar.thy
--- a/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:09:28 2012 +0200
+++ b/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:39:48 2012 +0200
@@ -525,6 +525,16 @@
 \end{quote}
 The \texttt{isabelle} environment is the one defined in the standard file
 \texttt{isabelle.sty} which most likely you are loading anyway.
+
+
+\section{Antiquotation}
+
+You want to show a constant and its type? Instead of going
+\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
+you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
+\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
+\verb!@!\verb!{const_typ length}! produces @{const_typ length}.
+
 *}
 
 (*<*)
diff -r 34ada66545ca -r 8262d35eff20 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:09:28 2012 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:39:48 2012 +0200
@@ -97,5 +97,21 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
+setup{*
+  let
+    fun pretty ctxt c =
+      let val tc = Proof_Context.read_const_proper ctxt false c
+      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
+      end
+  in
+    Thy_Output.antiquotation @{binding "const_typ"}
+     (Scan.lift Args.name_source)
+       (fn {source = src, context = ctxt, ...} => fn arg =>
+          Thy_Output.output ctxt
+            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
+  end;
+*}
+
 end
 (*>*)
\ No newline at end of file