# HG changeset patch
# User wenzelm
# Date 1117533191 -7200
# Node ID 6a449deff8d9dcc463645c093336b71d966617f5
# Parent  c0916ed7b8e9c2b763d65904f07acc26b1eadafe
antiquotations: added options short_names, unique_names;

diff -r c0916ed7b8e9 -r 6a449deff8d9 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Tue May 31 11:53:10 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Tue May 31 11:53:11 2005 +0200
@@ -547,6 +547,12 @@
 \item[$show_structs = bool$] controls printing of implicit structures.
 \item[$long_names = bool$] forces names of types and constants etc.\ to be
   printed in their fully qualified internal form.
+\item[$short_names = bool$] forces names of types and constants etc.\ to be
+  printed unqualified.  Note that internalizing the output again in the
+  current context may well yield a different result.
+\item[$unique_names = bool$] determines whether the printed version of
+  qualified names should be made sufficiently long to avoid overlap with names
+  declared further back.  Set to $false$ for more concise output.
 \item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
 \item[$display = bool$] indicates if the text is to be output as multi-line
   ``display material'', rather than a small piece of text without line breaks