1.1 --- a/doc-src/IsarImplementation/implementation.tex Thu May 08 23:07:15 2008 +0200
1.2 +++ b/doc-src/IsarImplementation/implementation.tex Fri May 09 12:44:31 2008 +0200
1.3 @@ -5,7 +5,7 @@
1.4 \usepackage{latexsym,graphicx}
1.5 \usepackage[refpage]{nomencl}
1.6 \usepackage{../iman,../extra,../isar,../proof}
1.7 -\usepackage[nohyphen,strings]{underscore}
1.8 +\usepackage[nohyphen,strings]{../underscore}
1.9 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
1.10 \usepackage{style}
1.11 \usepackage{../pdfsetup}
2.1 --- a/doc-src/IsarRef/isar-ref.tex Thu May 08 23:07:15 2008 +0200
2.2 +++ b/doc-src/IsarRef/isar-ref.tex Fri May 09 12:44:31 2008 +0200
2.3 @@ -4,7 +4,7 @@
2.4 \documentclass[12pt,a4paper,fleqn]{report}
2.5 \usepackage{latexsym,graphicx}
2.6 \usepackage{../iman,../extra,../isar,../proof}
2.7 -\usepackage[nohyphen,strings]{underscore}
2.8 +\usepackage[nohyphen,strings]{../underscore}
2.9 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
2.10 \usepackage{../ttbox,,../rail,../railsetup}
2.11 \usepackage{style}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/underscore.sty Fri May 09 12:44:31 2008 +0200
3.3 @@ -0,0 +1,248 @@
3.4 +% underscore.sty 21-Sep-2005 Donald Arseneau asnd@triumf.ca
3.5 +% Make the "_" character print as "\textunderscore" in text.
3.6 +% Copyright 1998,2001,2005,2006 Donald Arseneau;
3.7 +% License: LPPL version 1.2 or later.
3.8 +% Instructions follow after the definitions.
3.9 +
3.10 +\ProvidesPackage{underscore}[2006/09/13]
3.11 +
3.12 +\begingroup
3.13 + \catcode`\_=\active
3.14 + \gdef _{% \relax % No relax gives a small vulnerability in alignments
3.15 + \ifx\if@safe@actives\iftrue % must be outermost test!
3.16 + \string_%
3.17 + \else
3.18 + \ifx\protect\@typeset@protect
3.19 + \ifmmode \sb \else \BreakableUnderscore \fi
3.20 + \else
3.21 + \ifx\protect\@unexpandable@protect \noexpand_%
3.22 + \else \protect_%
3.23 + \fi\fi
3.24 + \fi}
3.25 + \global\let\ActiveUnderscore=_
3.26 + \gdef\normalUnderscoreDef{\let_\ActiveUnderscore}
3.27 +\endgroup
3.28 +
3.29 +% At begin: set catcode; fix \long \ttdefault so I can use it in comparisons;
3.30 +% reapply definition of active _ in output routine (\@firstofone to strip
3.31 +% away braces, so avoiding deeper nesting).
3.32 +\AtBeginDocument{%
3.33 + {\immediate\write\@auxout{\catcode\number\string`\_ \string\active}}%
3.34 + \catcode\string`\_\string=\active
3.35 + \edef\ttdefault{\ttdefault}%
3.36 + \output=\expandafter\expandafter\expandafter
3.37 + {\expandafter\expandafter\expandafter\normalUnderscoreDef
3.38 + \expandafter\@firstofone\the\output}%
3.39 +}
3.40 +
3.41 +\newcommand{\BreakableUnderscore}{\leavevmode\nobreak\hskip\z@skip
3.42 + \ifx\f@family\ttdefault \string_\else \textunderscore\fi
3.43 + \usc@dischyph\nobreak\hskip\z@skip}
3.44 +
3.45 +\DeclareRobustCommand{\_}{%
3.46 + \ifmmode \nfss@text{\textunderscore}\else \BreakableUnderscore \fi}
3.47 +
3.48 +
3.49 +\let\usc@dischyph\@dischyph
3.50 +\DeclareOption{nohyphen}{\def\usc@dischyph{\discretionary{}{}{}}}
3.51 +\DeclareOption{strings}{\catcode`\_=\active}
3.52 +
3.53 +\ProcessOptions
3.54 +\ifnum\catcode`\_=\active\else \endinput \fi
3.55 +
3.56 +%%%%%%%% Redefine commands that use character strings %%%%%%%%
3.57 +
3.58 +\@ifundefined{UnderscoreCommands}{\let\UnderscoreCommands\@empty}{}
3.59 +\expandafter\def\expandafter\UnderscoreCommands\expandafter{%
3.60 + \UnderscoreCommands
3.61 + \do\include \do\includeonly
3.62 + \do\@input \do\@iinput \do\InputIfFileExists
3.63 + \do\ref \do\pageref \do\newlabel
3.64 + \do\bibitem \do\@bibitem \do\cite \do\nocite \do\bibcite
3.65 + \do\Ginclude@graphics \do\@setckpt
3.66 +}
3.67 +
3.68 +% Macro to redefine a macro to pre-process its string argument
3.69 +% with \protect -> \string.
3.70 +\def\do#1{% Avoid double processing if user includes command twice!
3.71 + \@ifundefined{US\string_\expandafter\@gobble\string#1}{%
3.72 + \edef\@tempb{\meaning#1}% Check if macro is just a protection shell...
3.73 + \def\@tempc{\protect}%
3.74 + \edef\@tempc{\meaning\@tempc\string#1\space\space}%
3.75 + \ifx\@tempb\@tempc % just a shell: hook into the protected inner command
3.76 + \expandafter\do
3.77 + \csname \expandafter\@gobble\string#1 \expandafter\endcsname
3.78 + \else % Check if macro takes an optional argument
3.79 + \def\@tempc{\@ifnextchar[}%
3.80 + \edef\@tempa{\def\noexpand\@tempa####1\meaning\@tempc}%
3.81 + \@tempa##2##3\@tempa{##2\relax}%
3.82 + \edef\@tempb{\meaning#1\meaning\@tempc}%
3.83 + \edef\@tempc{\noexpand\@tempd \csname
3.84 + US\string_\expandafter\@gobble\string#1\endcsname}%
3.85 + \if \expandafter\@tempa\@tempb \relax 12\@tempa % then no optional arg
3.86 + \@tempc #1\US@prot
3.87 + \else % There is optional arg
3.88 + \@tempc #1\US@protopt
3.89 + \fi
3.90 + \fi
3.91 + }{}}
3.92 +
3.93 +\def\@tempd#1#2#3{\let#1#2\def#2{#3#1}}
3.94 +
3.95 +\def\US@prot#1#2{\let\@@protect\protect \let\protect\string
3.96 + \edef\US@temp##1{##1{#2}}\restore@protect\US@temp#1}
3.97 +\def\US@protopt#1{\@ifnextchar[{\US@protarg#1}{\US@prot#1}}
3.98 +\def\US@protarg #1[#2]{\US@prot{{#1[#2]}}}
3.99 +
3.100 +\UnderscoreCommands
3.101 +\let\do\relax \let\@tempd\relax % un-do
3.102 +
3.103 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3.104 +
3.105 +\endinput
3.106 +
3.107 +underscore.sty 13-Sep-2006 Donald Arseneau
3.108 +
3.109 +Features:
3.110 +~~~~~~~~~
3.111 +The "\_" command (which normally prints an underscore character or
3.112 +facsimile) is altered so that the hyphenation of constituent words
3.113 +is not affected, and hyphenation is permitted after the underscore.
3.114 +For example, "compound\_fracture" hyphenates as com- pound\_- frac- ture.
3.115 +If you prefer the underscore to break without a hyphen (but still with
3.116 +the same rules for explicit hyphen-breaks) then use the [nohyphen]
3.117 +package option.
3.118 +
3.119 +A simple "_" acts just like "\_" in text mode, but makes a subscript
3.120 +in math mode: activation_energy $E_a$
3.121 +
3.122 +Both forms use an underscore character if the font encoding contains
3.123 +one (e.g., "\usepackage[T1]{fontenc}" or typewriter fonts in any encoding),
3.124 +but they use a rule if there is no proper character.
3.125 +
3.126 +Deficiencies:
3.127 +~~~~~~~~~~~~~
3.128 +The skips and penalties ruin any kerning with the underscore character
3.129 +(when a character is used). However, there doesn't seem to be much, if
3.130 +any, such kerning in the ec fonts, and there is never any kerning with
3.131 +a rule.
3.132 +
3.133 +You must avoid "_" in file names and in cite or ref tags, or you must use
3.134 +the babel package, with its active-character controls, or you must give
3.135 +the [strings] option, which attempts to redefine several commands (and
3.136 +may not work perfectly). Even without the [strings] option or babel, you
3.137 +can use occasional underscores like: "\include{file\string_name}".
3.138 +
3.139 +Option: [strings]
3.140 +~~~~~~~~~~~~~~~~~
3.141 +The default operation is quite simple and needs no customization; but
3.142 +you must avoid using "_" in any place where LaTeX uses an argument as
3.143 +a string of characters for some control function or as a name. These
3.144 +include the tags for "\cite" and "\ref", file names for "\input",
3.145 +"\include", and "\includegraphics", environment names, counter names,
3.146 +and placement parameters (like "[t]"). The problem with these contexts
3.147 +is that they are `moving arguments' but LaTeX does not `switch on' the
3.148 +"\protect" mechanism for them.
3.149 +
3.150 +If you need to use the underscore character in these places, the package
3.151 +option [strings] is provided to redefine commands that take such a string
3.152 +argument so that protection is applied (with "\protect" being "\string").
3.153 +The list of commands is given in "\UnderscoreCommands", with "\do" before
3.154 +each; plus several others covering "\input", "\includegraphics, "\cite",
3.155 +"\ref", and their variants. Not included are many commands regarding font
3.156 +names, everything with counter names, environment names, page styles, and
3.157 +versions of "\ref" and "\cite" defined by external packages (e.g., "\vref"
3.158 +and "\citeyear").
3.159 +
3.160 +You can add to the list of supported commands by defining "\UnderscoreCommands"
3.161 +before loading this package; e.g.
3.162 +
3.163 + \usepackage{chicago}
3.164 + \newcommand{\UnderscoreCommands}{% (\cite already done)
3.165 + \do\citeNP \do\citeA \do\citeANP \do\citeN \do\shortcite
3.166 + \do\shortciteNP \do\shortciteA \do\shortciteANP \do\shortciteN
3.167 + \do\citeyear \do\citeyearNP
3.168 + }
3.169 + \usepackage[strings]{underscore}
3.170 +
3.171 +Not all commands can be supported this way! Only commands that take a
3.172 +string argument *first* can be protected. One optional argument before
3.173 +the string argument is also permitted, as exemplified by "\cite": both
3.174 +"\cite{tags}" and "\cite[text]{tags}" are allowed. A command like
3.175 +"\@addtoreset" which takes two counter names as arguments could not
3.176 +be protected by listing it in "\UnderscoreCommands".
3.177 +
3.178 +*When you use the [strings] option, you must load this package
3.179 +last* (or nearly last).
3.180 +
3.181 +There are two reasons: 1) The redefinitions done for protection must come
3.182 +after other packages define their customized versions of those commands.
3.183 +2) The [strings] option requires the "_" character to be activated immediately
3.184 +in order for the cite and ref tags to be read properly from the .aux file
3.185 +as plain strings, and this catcode setting might disrupt other packages.
3.186 +
3.187 +The babel package implements a protection mechanism for many commands,
3.188 +and will be a complete fix for most documents without the [strings] option.
3.189 +Many add-on packages are compatible with babel, so they will get the
3.190 +strings protection also. However, there are several commands that are
3.191 +not covered by babel, but can easily be supported by the [strings] and
3.192 +"\UnderscoreCommands" mechanism. Beware that using both [strings] and
3.193 +babel might lead to conflicts, but none are seen yet (load babel last).
3.194 +
3.195 +Implementation Notes:
3.196 +~~~~~~~~~~~~~~~~~~~~~
3.197 +The first setting of "_" to be an active character is performed in a local
3.198 +group so as to not interfere with other packages. The catcode setting
3.199 +is repeated with "\AtBeginDocument" so the definition is in effect for the
3.200 +text. However, the catcode setting is repeated immediately when the
3.201 +[strings] option is detected.
3.202 +
3.203 +The definition of the active "_" is essentially:
3.204 +
3.205 + \ifmmode \sb \else \BreakableUnderscore \fi
3.206 +
3.207 +where "\sb" retains the normal subscript meaning of "_" and where
3.208 +"\BreakableUnderscore" is essentially "\_". The rest of the definition
3.209 +handles the "\protect"ion without causing "\relax" to be inserted before
3.210 +the character.
3.211 +
3.212 +"\BreakableUnderscore" uses "\nobreak\hskip\z@skip" to separate the
3.213 +underscore from surrounding words, thus allowing TeX to hyphenate them,
3.214 +but preventing free breaks around the underscore. Next, it checks the
3.215 +current font family, and uses the underscore character from tt fonts or
3.216 +otherwise "\textunderscore" (which is a character or rule depending on
3.217 +the font encoding). After the underscore, it inserts a discretionary
3.218 +hyphenation point as "\usc@dischyph", which is usually just "\-"
3.219 +except that it still works in the tabbing environment, although it
3.220 +will give "\discretionary{}{}{}" under the [nohyphen] option. After
3.221 +that, another piece of non-breaking interword glue is inserted.
3.222 +Ordinarily, the comparison "\ifx\f@family\ttdefault" will always fail
3.223 +because "\ttdefault" is `long' whereas "\f@family" is not (boooo hisss),
3.224 +but "\ttdefault" is redefined to be non-long by "\AtBeginDocument".
3.225 +
3.226 +The "\_" command is then defined to use "\BreakableUnderscore".
3.227 +
3.228 +If the [strings] option is not given, then that is all!
3.229 +
3.230 +Under the [strings] option, the list of special commands is processed to:
3.231 +
3.232 + - retain the original command as "\US_"*command* (e.g., "\US_ref")
3.233 + - redefine the command as "\US@prot\US_command" for ordinary commands
3.234 + ("\US@prot\US_ref") or as "\US@protopt\US_command" when an optional
3.235 + argument is possible (e.g., "\US@protopt\US_bibitem").
3.236 + - self-protecting commands ("\cite") retain their self-protection.
3.237 +
3.238 +Diagnosing the state of the pre-existing command is done by painful
3.239 +contortions involving "\meaning".
3.240 +
3.241 +"\US@prot" and "\US@protopt" read the argument, process it with
3.242 +"\protect" enabled, then invoke the saved "\US_command".
3.243 +
3.244 +Modifications:
3.245 +~~~~~~~~~~~~~~
3.246 +13-Sep-2006 Reassert my definition in the output routine (listings).
3.247 +21-Sep-2005 \includegraphics safe.
3.248 +12-Oct-2001 Babel (safe@actives) compatibility and [nohyphen] option.
3.249 +
3.250 +Test file integrity: ASCII 32-57, 58-126: !"#$%&'()*+,-./0123456789
3.251 +:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~