diff --git a/.#todo.org b/.#todo.org deleted file mode 120000 index a4bcf93..0000000 --- a/.#todo.org +++ /dev/null @@ -1 +0,0 @@ -user@thinkgentoo.29142:1592891722 \ No newline at end of file diff --git a/tesi/Makefile b/tesi/Makefile index 7e4f052..23b8767 100644 --- a/tesi/Makefile +++ b/tesi/Makefile @@ -12,8 +12,6 @@ tesi: emacs -batch tesi_unicode.org -f org-latex-export-to-latex --kill python3 conv.py tesi_unicode.tex tesi.tex pdflatex $(SRC) - bibtex $(AUX) - pdflatex $(SRC) pdflatex $(SRC) @echo @echo "=== All done. Generated $(NAME).pdf ===" diff --git a/tesi/conv.py b/tesi/conv.py index 8143856..53584c7 100644 --- a/tesi/conv.py +++ b/tesi/conv.py @@ -7,7 +7,7 @@ try: except: allsymbols = json.load(open('../unicode-latex.json')) -mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', '₄', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆', '↦' ] +mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', '₄', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆', '↦', 'Θ', 'ρ', '⇒', '∑', '⊧' ] extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'} diff --git a/tesi/ltximg/org-ltximg_241c2a1bb1e1c87f00fb4e00188866e32e2d5196.png b/tesi/ltximg/org-ltximg_241c2a1bb1e1c87f00fb4e00188866e32e2d5196.png new file mode 100644 index 0000000..af78ea0 Binary files /dev/null and b/tesi/ltximg/org-ltximg_241c2a1bb1e1c87f00fb4e00188866e32e2d5196.png differ diff --git a/tesi/ltximg/org-ltximg_259cd9c29679ee2346a4e50a384df6152c86dc0d.png b/tesi/ltximg/org-ltximg_259cd9c29679ee2346a4e50a384df6152c86dc0d.png new file mode 100644 index 0000000..0930267 Binary files /dev/null and b/tesi/ltximg/org-ltximg_259cd9c29679ee2346a4e50a384df6152c86dc0d.png differ diff --git a/tesi/ltximg/org-ltximg_47652b0773cf35233f7997aecd859d034f8eeda2.png b/tesi/ltximg/org-ltximg_47652b0773cf35233f7997aecd859d034f8eeda2.png new file mode 100644 index 0000000..ce2a4f9 Binary files /dev/null and b/tesi/ltximg/org-ltximg_47652b0773cf35233f7997aecd859d034f8eeda2.png differ diff --git a/tesi/ltximg/org-ltximg_7cdc2266aa831645dee41ce51b799c205d4a513b.png b/tesi/ltximg/org-ltximg_7cdc2266aa831645dee41ce51b799c205d4a513b.png new file mode 100644 index 0000000..5e90eb1 Binary files /dev/null and b/tesi/ltximg/org-ltximg_7cdc2266aa831645dee41ce51b799c205d4a513b.png differ diff --git a/tesi/ltximg/org-ltximg_8673d3b97cfa5fd140fb4a665c533060ef3858c0.png b/tesi/ltximg/org-ltximg_8673d3b97cfa5fd140fb4a665c533060ef3858c0.png new file mode 100644 index 0000000..d731db7 Binary files /dev/null and b/tesi/ltximg/org-ltximg_8673d3b97cfa5fd140fb4a665c533060ef3858c0.png differ diff --git a/tesi/ltximg/org-ltximg_d69e7d4a12dea954ee165c1f3edf30bd72f17b5d.png b/tesi/ltximg/org-ltximg_d69e7d4a12dea954ee165c1f3edf30bd72f17b5d.png new file mode 100644 index 0000000..8ea5b86 Binary files /dev/null and b/tesi/ltximg/org-ltximg_d69e7d4a12dea954ee165c1f3edf30bd72f17b5d.png differ diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 5ecb687..987c9fb 100644 Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index 30f232a..a825d53 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1,7 +1,7 @@ \begin{comment} TODO: not all todos are explicit. Check every comment section TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerenti -* TODO Scaletta [1/5] +* TODO Scaletta [2/4] - [X] Introduction - [-] Background [80%] - [X] Low level representation @@ -9,17 +9,19 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent - [X] Pattern matching - [X] Symbolic execution - [ ] Translation Validation - - [-] Translation validation of the Pattern Matching Compiler + - [X] Translation validation of the Pattern Matching Compiler - [X] Source translation - [X] Formal Grammar - [X] Compilation of source patterns - - [ ] Target translation - - [ ] Formal Grammar - - [ ] Symbolic execution of the Lambda target + - [X] Target translation + - [X] Formal Grammar + - [X] Symbolic execution of the Lambda target - [X] Equivalence between source and target - - [ ] Practical results + - [ ] Examples + - [ ] esempi + - [ ] cosa manca per essere incorporata + - [ ] Considerazioni? - \end{comment} #+TITLE: Translation Verification of the OCaml pattern matching compiler @@ -74,13 +76,12 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent #+LaTeX_HEADER: xleftmargin=1em, #+LaTeX_HEADER: } #+LaTeX_HEADER: \lstset{aboveskip=0.4ex,belowskip=0.4ex} - #+EXPORT_SELECT_TAGS: export #+EXPORT_EXCLUDE_TAGS: noexport #+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t #+STARTUP: showall -\section{Introduction} +\section{Introduction} This dissertation presents an algorithm for the translation validation of the OCaml pattern matching compiler. Given a source program and its compiled version the algorithm checks whether the two are equivalent or produce a counter @@ -90,14 +91,6 @@ language and implemented a prototype equivalence checker along with a formal statement of correctness and its proof. The prototype is to be included in the OCaml compiler infrastructure and will aid the development. -\begin{comment} -TODO: should this be removed? -Our equivalence algorithm works with decision trees. Source patterns are -converted into a decision tree using a matrix decomposition algorithm. -Target programs, described in the Lambda intermediate -representation language of the OCaml compiler, are turned into decision trees -by applying symbolic execution. -\end{comment} \subsection{Motivation} Pattern matching in computer science is a @@ -105,7 +98,7 @@ widely employed technique for describing computation as well as deduction. Pattern matching is central in many programming languages such as the ML family languages, Haskell and Scala, different model checkers, such as Murphi, and proof assistants such as Coq and -Isabelle. Recently the C++ community is considering [CIT] adding the +Isabelle. Recently the C++ community is considering\cite{cpp_pat} adding the support for pattern matching in the compiler. The work done in this thesis provides a general method that is agnostic with respect to the compiler implementation and the language used. @@ -459,8 +452,8 @@ oriented language such as C, C++ and Java, such as: For example the principal type of the List.length function is "For any /a/, function from list of /a/ to /int/" and /a/ is called the /type parameter/. - Strong typing: Languages such as C and C++ allow the programmer to operate on data - without considering its type, mainly through pointers[CIT]. Other languages such as Swift - and Java performs type erasure[CIT] so at runtime the type of the data can't be queried. + without considering its type, mainly through pointers\cite{andrei}. Other languages such as Swift + and Java performs type erasure\cite{java,swift} so at runtime the type of the data can't be queried. In the case of programming languages using an Hindley-Milner type system the programmer is not allowed to operate on data by ignoring or promoting its type. - Type Inference: the principal type of a well formed term can be inferred without any @@ -482,7 +475,7 @@ although mutable statements and imperative constructs are permitted. In addition to that OCaml features an object system, that provides inheritance, subtyping and dynamic binding, and modules, that provide a way to encapsulate definitions. Modules are checked -statically and can be reifycated through functors[CIT]. +statically and can be reifycated through functors\cite{tantalizing}. ** Compiling OCaml code @@ -496,20 +489,17 @@ is trasformed into an untyped syntax tree. Code with syntax errors is rejected at this stage. After that the AST is processed by the type checker that performs three steps at once: -- type inference, using the classical /Algorithm W/[CIT] +- type inference, using the classical /Algorithm W/\cite{comp_pat} - perform subtyping and gathers type information from the module system - ensures that the code obeys the rule of the OCaml type system At this stage, incorrectly typed code is rejected. In case of success, the untyped AST in trasformed into a /Typed Tree/. After the typechecker has proven that the program is type safe, the compiler lower the code to /Lambda/, an s-expression based -language that assumes that its input has already been proved safe[CIT]. +language that assumes that its input has already been proved safe\cite{dolan}. After the Lambda pass, the Lambda code is either translated into bytecode or goes through a series of optimization steps performed by -the /Flambda/ optimizer[CIT] before being translated into assembly. -\begin{comment} -TODO: Talk about flambda passes? -\end{comment} +the /Flambda/ optimizer\cite{flambda} before being translated into assembly. This is an overview of the different compiler steps. [[./files/ocamlcompilation.png]] @@ -660,8 +650,6 @@ intermediate language can change across compiler releases. Spiega che la sintassi che supporti e` quella nella BNF \end{comment} - - ** Pattern matching Pattern matching is a widely adopted mechanism to interact with ADT[CIT]. C family languages provide branching on predicates through the use of @@ -736,7 +724,7 @@ domain of all possible inputs of a program, detecting infeasible paths, dead code and proving that two code segments are equivalent. \\ Let's take as example this signedness bug that was found in the -FreeBSD kernel [CIT] and allowed, when calling the /getpeername/ function, to +FreeBSD kernel\cite{freebsd} and allowed, when calling the /getpeername/ function, to read portions of kernel memory. \begin{comment} TODO: controlla paginazione @@ -850,7 +838,7 @@ feasible[CIT] and in case of explosion usually symbolic execution engines implement heuristics to reduce the size of the search space.[CIT] ** Translation Validation -Translators, such as translators and code generators, are huge pieces of +Translators, such as compilers and code generators, are huge pieces of software usually consisting of multiple subsystem and constructing an actual specification of a translator implementation for formal validation is a very long task. Moreover, different @@ -858,12 +846,48 @@ translators implement different algorithms, so the correctness proof of a translator cannot be generalized and reused to prove another translator. Translation validation is an alternative to the verification of existing translators that consists of taking the source and the target -(compiled) program and proving /a posteriori/ their semantic equivalence. -\\ -- [ ] Techniques for translation validation -- [ ] What does semantically equivalent mean -- [ ] What happens when there is no semantic equivalence -- [ ] Translation validation through symbolic execution +(compiled) program and proving /a posteriori/ their semantic +equivalence. + +\subsubsection{Translation Validation as Transation Systems} +There are many successful attempts at translation validation of code +translators[CIT] and to a less varying degree of compilers[CIT]. +Pnueli et al. provide a computational model based on synchronous +transition systems to prove a translation verification tool +based on the following model. +[[./files/translation.png]] +The description of the computational models resembles closely the one +in [CIT]. +A synchronous transition system (STS) A = (V, Θ, ρ) where +- V: is a finite set of variables; ∑ᵥ is the set of all states over V +- Θ: a satisfiable assertion over the state variables of A, + representing its initial state +- ρ: a transition relation computed as an assertion ρ(V, V') that + relates a state s∈∑ᵥ to the successor s'∈∑ᵥ +A computation of A is an infinite sequence σ = (s₀, s₁, s₂, ...) where +| ∀i∈ℕ sᵢ∈∑ᵥ +| s₀⊧Θ +| ∀i∈ℕ (sᵢ, s_{i+1+})⊧ρ +We can give a notion of correct implementation of the Source to Target +compiler in the translation validation settings by using the concept +of refinement between STS. +Let A = (V_{A}, Θ_{A}, ρ_{A}, E_{A}) and C = (V_{C}, Θ_{C}, ρ_{C}, E_{C}) +be an abstract and a concrete STS where E_{A}⊆V_{A} and E_{C}⊆V_{C} +and are externally observable variables. +We call a projection s^{F} the state s projected on the subset F⊆V. +An observation of a STS is any infinite sequence of the form +(s_{0}^{E}, s_{1}^{E}, s_{2}^{E}, ...) for a path σ = (s₀, s₁, s₂, ...). +We say that the concrete STS C refines the abstract STS A if +Obs(C)⊆Obs(A). +If we can prove a correct mapping of state variables at the target and +source levels (as highlighted by the figure) by a function map: +V_{A}↦V_{C} we can use inductively prove equivalence using a +simulation relation: +| $\bigwedge_{s\in{V_A^S}}s = map(s) \wedge \Theta_{C} \Rightarrow \Theta_{A}$ (initial condition) +| $\bigwedge_{i\in{V_A^I}}i \wedge \bigwedge_{s\in{V_A^S}}s = map(s) \wedge \rho_{A} \wedge \rho_{C} \Rightarrow$ +| \quad\quad $\bigwedge_{i\in{V_A^S}}s' \wedge \bigwedge_{o\in{V_A^O}}o' = map(o')$ (step) +Proof is out of scope for this thesis. +Our work uses bisimulation to prove equivalence. * Translation Validation of the Pattern Matching Compiler ** Accessors @@ -904,7 +928,7 @@ TODO: metti linea qualcosa a dividere \end{comment} Primitive OCaml datatypes include aggregate types in the form of /tuples/ and /lists/. Other aggregate types are built using module -functors. [CIT] +functors\cite{ovla}. Low level /Lambda/ untyped constructors of the form #+BEGIN_SRC type t = Constant | Block of int * t @@ -1543,9 +1567,9 @@ We formalize this intuition as follows constructor k, we have: | if k = kₖ \text{ for some k then} - | \quad m(vᵢ)ⁱ = mₖ((v_{l}')ˡ +++ (v_{i})^{i∈I\DZ}) + | \quad m(vᵢ)ⁱ = mₖ((v_{l}')ˡ +++ (v_{i})^{i∈I$\backslash\text{\{0\}}$}) | \text{else} - | \quad m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\DZ} + | \quad m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I$\backslash\text{\{0\}}$} \begin{comment} TODO: fix \{0} @@ -1651,11 +1675,11 @@ possible values that the type of the function can hold. D? is the fallback node of the tree that is taken whenever the value at that point of the execution can't flow to any other subbranch. Intuitively, the π_{fallback} condition of the D? fallback node is -| π_{fallback} = ¬\bigcup\limits_{i∈I}πᵢ +| $\pi_{fallback} = \neg\bigcup\limits_{i\in I}\pi_i$ The fallback node can be omitted in the case where the domain of the children nodes correspond to set of possible values pointed by the accessor at that point of the execution -| domain(vₛ(a)) = \bigcup\limits_{i∈I}πᵢ +| $domain(v_s(a)) = \bigcup\limits_{i\in I}pi_i$ We say that a translation of a target program to a decision tree is correct when for every possible input, the target program and its respective decision tree produces the same result @@ -2084,7 +2108,7 @@ I think the unreachable case should go at the end. | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I 4. When we have a Switch on the right we define π_{fallback} as the domain of values not covered but the union of the constructors kᵢ - | π_{fallback} = ¬\bigcup\limits_{i∈I}π(kᵢ) + | $\pi_{fallback} = \neg\bigcup\limits_{i\in I}\pi(k_i)$ Our algorithm proceeds by trimming | equiv(S, Switch(a, (kᵢ → Cₛᵢ)^{i∈I}, C_{sf}), Cₜ) := | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), Cₛ, C_{a→π_{fallback}})) @@ -2108,3 +2132,89 @@ I think the unreachable case should go at the end. | Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) that is enough for proving that | Cₛₖ(vₛ) ≠ (C_{t/a→πₖ}(vₜ) = Cₜ(vₜ)) + +* Examples +In this section we discuss some examples given as input and output of +the prototype tool. +\par\noindent\rule{\textwidth}{0.4pt} +\begin{lstlisting} +external observe : int -> int = "observe" + +let mm = function + | 2 -> observe 2 + | 3 -> observe 3 + | 4 -> observe 4 + | _ -> observe 5 +\end{lstlisting} +\par\noindent\rule{\textwidth}{0.4pt} +\begin{lstlisting} +(setglobal Example0! + (let + (mm/81 = + (function param/82[int] : int + (catch + (let (switcher/85 =a (-2+ param/82)) + (if (isout 2 switcher/85) (exit 1) + (switch* switcher/85 + case int 0: (observe 2) + case int 1: (observe 3) + case int 2: (observe 4)))) + with (1) (observe 5)))) + (makeblock 0 mm/81))) +\end{lstlisting} +\par\noindent\rule{\textwidth}{0.4pt} + +\begin{lstlisting} +\end{lstlisting} + + +\begin{thebibliography}{9} +\bibitem{cpp_pat} +Sergei Murzin, Michael Park, David Sankel, Dan Sarginson. +\textit{P1371R1: Pattern Matching Proposal for C++}. +http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1371r1.pdf + +\bibitem{swift} +Nayebi, Fatih. +\textit{Swift Functional Programming}. +Packt Publishing Ltd, 2017. + +\bibitem{java} +Radenski, Atanas, Jeff Furlong, Vladimir Zanev. +\textit{The Java 5 generics compromise orthogonality to keep compatibility}. +Journal of Systems and Software 81.11 (2008): 2069-2078. + +\bibitem{andrei} +Alexandrescu, Andrei. +\textit{Modern C++ design: generic programming and design patterns applied}. +Addison-Wesley, 2001. + +\bibitem{tantalizing} +Yallop, Jeremy, and Oleg Kiselyov. +\textit{First-class modules: hidden power and tantalizing promises}. +Workshop on ML. Vol. 2. 2010. + +\bibitem{comp_pat} +Augustsson, Lennart. +\textit{Compiling pattern matching}. +Conference on Functional Programming Languages and Computer Architecture. Springer, Berlin, Heidelberg, 1985. + +\bibitem{dolan} +Dolan, Stephen. +\textit{Malfunctional programming}. +ML Workshop. 2016. + +\bibitem{flambda} +OCaml core developers. +\textit{OCaml Manual} +http://caml.inria.fr/pub/docs/manual-ocaml/flambda.html + +\bibitem{freebsd} +https://www.cvedetails.com/cve/CVE-2002-0973/ + +\bibitem{ovla} +Charguéraud, A., Filliâtre, J. C., Pereira, M., Pottier F. (2017). +\textit{VOCAL–A Verified OCAml Library}. +https://hal.inria.fr/hal-01561094/ + +\end{thebibliography} diff --git a/tesi/ulem.ltx b/tesi/ulem.ltx new file mode 100644 index 0000000..4d46a2f --- /dev/null +++ b/tesi/ulem.ltx @@ -0,0 +1,273 @@ +% +% ulem.ltx Manual for ulem.sty +% +% +% Copyright (c) 1989-2019 by Donald Arseneau +% +% Version date 2019/11/18 +% +\documentclass[12pt]{ltxdoc} +\addtolength{\textwidth}{1cm} +%\makeshortverb`\| +\usepackage{ulem} +\def\baselinestretch{1.06} +\setlength\parskip{2pt} +\hyphenation{normalem uwforbf ulforem} +\title{The ulem package:\\ underlining for emphasis} +\author{Donald Arseneau\\ asnd@triumf.ca} +\date{2019/11/18} +\begin{document} + +\maketitle +\sloppy + +\begin{abstract} + The ulem package provides various types of underlining that can stretch + between words and be broken across lines. Use it with \LaTeX\ or plain \TeX. + + In \LaTeX, ulem normally replaces italics with underlining in text + emphasized by \cs{emph}, and to some extent by \cs{em}. A declaration + of |\normalem| or the |\usepackage| option |[normalem]| disables this + feature. + + The following commands are defined for general use:\\[5pt] + \indent \begin{tabular}{l@{\quad}l}\hline\noalign{\vskip2pt} + |\uline{important}| & underlined text like \uline{important}\\[1pt] + |\uuline{urgent}| & double-underlined text like \uuline{urgent}\\[1pt] + |\uwave{boat}| & wavy underline like {\let\ULleaders\cleaders\uwave{boat}}\\[1pt] + |\sout{wrong}| & line struck through word like \sout{wrong}\\[1pt] + |\xout{removed}| & marked over like \xout{removed} \\[1pt] + |\dashuline{dashing}|& dashed underline like \dashuline{dashing}\\[1pt] + |\dotuline{dotty}| & dotted underline like \dotuline{dotty}\\[3pt]\hline + \end{tabular}\\[6pt] + Other similar commands can be defined with relative ease by utilizing the + \cs{markoverwith} command provided by ulem. +\end{abstract} + + +\begin{footnotesize} +\noindent The ulem package is Copyright \copyright\ 1989--2019 by +Donald Arseneau (Vancouver, Canada).\\ +The package (ulem.sty) and this documentation (ulem.ltx, ulem.pdf) may be +freely transmitted, reproduced, or modified for any purpose provided that the +copyright notice is left intact. +(Small excerpts may of course be taken and used without any restriction.)\par +\end{footnotesize} + +\section{Basic Use} +Ulem is a package for \LaTeX\ or plain \TeX\ which provides various types of +underlining that can stretch between words and be broken across lines. +Such underlining is given by the \cs{uline} command, leaving the original +\cs{underline} command available for math mode. +To load this package in plain \TeX, use `|\input ulem.sty|'. + +In \LaTeX\ ulem replaces italics with underlining in text emphasized +by \cs{em} or \cs{emph} -- but only if the text is delimited by +braces. Unlike regular \cs{emph} emphasis, nested ulem emphasis generates +multiple underlining; it does not alternate on and off. +To use \cs{uline} for underlining, but have \cs{em} and \cs{emph} still +produce normal italics, load ulem with |\usepackage[normalem]{ulem}|, +or declare \cs{normalem} in the preamble. + +Unlike regular underlining, ulem allows line breaks, and manual +hyphenation, within the underlined text; but it is far from perfect. It is +most suitable for simple text like {\em \LaTeX: A document preparation +system\/} that may need to be underlined in a manuscript submitted for +publication. Again, ulem can only give underlined text for \cs{em} when +the text is delimited by explicit braces. + +The thickness of the underline rule is given by the command macro +\cs{ULthickness}; use \cs{renewcommand} (not the usual +\cs{setlength}) to change it.\footnote +{Users of plain \TeX\ should use \textbackslash def wherever these +instructions recommend \textbackslash(re)newcommand, and dimen +assignments wherever \textbackslash setlength is mentioned.}\, +The depth of the underline is controlled +by the length \cs{ULdepth}. The default value is a special flag +(\cs{maxdimen}) which lets the depth vary depending on the current font. +You can set a particular value to \cs{ULdepth} (using \cs{setlength}) to +force a particular depth, either locally for a special purpose, or +for the document as a whole. (See the definition of \cs{sout} for an +example.) + +Other types of underlining are defined as well: +a wavey underline with \cs{uwave} (\uwave{under-wave}), double underlines +using \cs{uuline} (\uuline{two lines under this}), dashed \cs{dashuline} +(\dashuline{dashes underneath}) or dotted \cs{dotuline} (\dotuline{dots +below}) underlines. Non-underlines are: a line to strike out text \cs{sout} +(\sout{strike out}), and text crossed-out with hatching \cs{xout} +(\xout{cross out}). See them tabulated in the abstract. + +Alternative package: soul. + +\section{Defining new commands} + +You can define your own styles of overprinting or underlining by using +the \cs{markoverwith} command in the definition of your new command. +The definition should be something like:\\[6pt] + \cs{newcommand}\cs{cmd}|{|\cs{bgroup} \meta{settings}\cs{markoverwith}|{|\meta{something}|}|\cs{ULon}|}|\\[8pt] +The `\meta{something}' can be as simple as a single character, or as complex as +you can keep track of; it will likely contain some repositioning commands, perhaps +\cs{raisebox}. + +Producing a colored underline or strike-through is not supported by +regular |\uline| or |\sout|, but it is quite easy to colorize using +the \cs{markoverwith} mechanism: just put |\textcolor{|\dots|}| in +the \meta{something}, such as this definition: +\begin{verbatim} + \newcommand\reduline{\bgroup\markoverwith + {\textcolor{red}{\rule[-0.5ex]{2pt}{0.4pt}}}\ULon} +\end{verbatim} +If you really feel the need to make a new command with a truly +flexible rule, then look in ulem.sty and copy from the definitions +of \cs{uline} and \cs{sout}. + +Any type of underlining can be substituted for any font-selection command +by issuing a proper \cs{useunder} declaration:\\[3pt] + \cs{useunder}|{|\meta{underlinecommand}|}{|\meta{fontdeclaration}|}{|\meta{fontcommand}|}|\\[3pt] +e.g., |\useunder{\uuline}{\bfseries}{\textbf}| gives a double underline +instead of bold face in \LaTeX\ (but note the problem explained next). + +The commands \cs{normalem} and \cs{ULforem} respectively disable and enable +underlining for \cs{em}/\cs{emph}, and so do the \cs{usepackage} +options [normalem] and [ULforem]. There is also the \cs{usepackage} +option [UWforbf] to replace boldface from \cs{textbf} with a wavey underline. +These features use the \cs{useunder} command internally. +UWforbf specifically employs +\cs{useunder}|{|\cs{uwave}|}|\allowbreak|{|\cs{bf}|}|\allowbreak|{|\cs{textbf}|}|, +so the \cs{bfseries} +command still produces bold face, but \cs{bf} makes an +under-wave (if \cs{bf} is defined at all). That is +because section title formatting typically uses \cs{bfseries} not delimited by +braces, which would give errors for \cs{uwave}.\footnote{%% no verbatim in footnotes +To get under-waved section titles (in ordinary \LaTeX\ classes) you could define:\\ +\texttt{\string\renewcommand\string\@seccntformat[1]\string{\string\uwave +\string{\string\csname\ the\#1\string\endcsname\string}\string\hskip 1em\string}}\\ +and later specify +\texttt{\string\section[...]\string{\string\uwave\string{...\string}\string}}. +But you don't want to enter that swamp.} +In plain \TeX\ there is \cs{bf} but no \cs{textbf} so you could say |\useunder{\uwave}{\bf}{}|. + +Some commands, such as |\\| and \cs{hskip} are given special treatment to +work within uline, but others are not. Support for others can sometimes +be added by assigning special meanings in the token register \cs{UL@hook}. +(In \LaTeX\ do +|\addto@hook\UL@hook{\let\cmd\|\textsl{UL-version-of-cmd}|}|.) The UL +versions of commands should be modelled on |\UL@hskip| or |\UL@cr|, and +should include the test `|\ifx\ \LA@space|'. For example, support for +\cs{marginpar} is added through the hook mechanism. + +All the underlining commands are robust in \LaTeX. + + +\section{Complications} +The various underlining commands are essentially textual, and will not +work quite the same in math mode. But since some font commands, +in the old-\LaTeX\ style (`oldlfont') serve both for text and math, +math mode is handled (in an approximate way). Generally, you should +avoid using ulem's commands within math, but math may appear in the +text argument to ulem's commands. + +Every word is typeset in an underlined box, so automatic hyphenation is +disabled, but explicit discretionary hyphens (|\-|) will still be +obeyed. Several text-formatting commands are specially supported within +the underlining: |\-|, |\ |, |~|, |\\|, |\newline|, |\linebreak|, +|\nolinebreak|, |\penalty|, |\hskip|, |\hspace|, |\hfil|, |\hfill|, |\hss|. +Displayed math is not supported. The special commands +do have a problem: they end a group so any local assignments are lost. + +The underlines continue between words, and stretch just like ordinary +spaces do. Since spaces delimit words, there may be some difficulty +with syntactical spaces (e.g. `|2.3 pt|'). Some effort is made to handle +such cases, but sometimes (such as |\let\x= y|) the space is interpreted +incorrectly. You can usually solve the problem by enclosing the offending +command in braces or in a macro (like |\newcommand\xeqy{\let\x= y}|), +but\,\dots + +One important incompatibility with braces and macro replacement: +\textbf{All the text in braces or coming from a macro is typeset in a box} +(as if in \cs{mbox}). Consequently, +braces will suppress stretching and line-breaking in the text they +enclose. Moreover, the specially-handled commands |\-|, |\\|, |\newline| +and |\linebreak| are usually ignored if they appear inside extra braces. +They operate only when the braces delimit a command parameter without +introducing a level of grouping. (Even though braces delimiting command +parameters do not normally imply grouping, many commands will add their +own grouping.) Thus, you should try to limit inner braces to short bits of +text or for delimiting parameters to commands. For emergency repairs, see +the sadistic `Marat/Sade' example below. Syntactical spaces inside braces +never cause a problem, nor do spaces in math mode. + +Text produced by expansion of a command (macro) is boxed too, but |\\|, |\ |, +and |\-| still work properly in the expansion text so that while\\[2pt] +\indent |\newcommand\iff{if and only if} ... \uline{\iff}|\\[2pt] +prevents stretching and line-breaking between words, the alternative\\[2pt] +\indent |\newcommand\iff{if\ and\ only\ if} ... \uline{\iff}|\\[2pt] +allows stretching and line-breaking. There is a remaining problem though: +the |\ | (backslash-space) between words closes a group and any local +assignments will be lost, in particular, font changes and color changes. + +This loss of local assignments will break some other standard commands, +(e.g., \cs{cite}) which produce multiple `words' using local assignments. +The way to protect such commands is to bury them in an \cs{mbox}: +\hskip 5pt plus 2in +|\emph{every\-one agrees~\mbox{\cite{you,me}}.}| + +With ULforem in effect, +nested \cs{em} or \cs{emph} commands produce multiple underlining, +but heed the warnings +about braces above. To get italics without underlining, use \cs{it}, +\cs{itshape}, or \cs{textit}. Nesting +of other types of underline is also possible, but the `underlines' may +overlap. + +\medskip +Here is a simple example (highlighting all invented words):\\[4pt] +\begin{minipage}[t]{.58\linewidth}\hbadness=9999 +\ttfamily \rightskip=0pt plus 2cm +|'Twas| |\emph{brillig}| |and| |the| |\emph{slithy~toves}| +|did| |\emph{gyre}| |and| |\emph{gim\-ble}| |in| |the| |\emph{wabe,\\| |}| +|All| |\emph{mim\-sey}| |were| |the| |\emph{boro\-goves}| |and| +|the| |\emph{mome| |raths| |outgrabe}.| +\end{minipage}\hfill +\begin{minipage}[t]{.4\linewidth}\hbadness=9999 +'Twas \emph{brillig} and the \emph{slithy~toves} +did \emph{gyre} and \emph{gim\-ble} in the \emph{wabe,\\ } +All \emph{mim\-sey} were the \emph{boro\-goves} and +the \emph{mome raths out\-grabe}.\par\mbox{} +\end{minipage}\vspace{6pt} +Note use +of explicit hyphenation in `gimble' and `borogoves', the tie (|~|) +that prevents a line break in `slithy toves', but stretches like a +usual space, the `|\\|' that gives a proper linebreak, and the regular +(unforced) linebreak in `mome raths outgrabe'. + +\medskip +Here is an ugly example showing how nested uline (\cs{emph}) needs +to be broken up to allow line-breaks\\[2pt] +\begin{minipage}[t]{.5\linewidth} +\ttfamily \rightskip=0pt plus 1.5cm \hbadness=9999 +|No,| |I| |did| |{\em| |not}| |act| |in| |the| |movie| |{\em| |\emph{The}| +|\emph{Persecution}| |\emph{and}| |\emph{Assassin}\-\emph{ation}| |\emph{of}| +|\emph{Jean-Paul}| |\emph{Marat},| |as| |Per\-formed| |by| |the| |Inmates| +|of| |the| |Asylum| |of| |Charenton| |Under| |the| |Direc\-tion| |of| |the| +|Marquis| |de~Sade!}| |But| |I| |{\em| |did}| |see| |it.|\\\mbox{} +\end{minipage}\hfill +\begin{minipage}[t]{.43\linewidth}\hbadness=9999 +No, I did {\em not} act in the movie {\em \emph{The} +\emph{Persecution} \emph{and} \emph{Assassin}\-\emph{ation} \emph{of} +\emph{Jean-Paul} \emph{Marat}, as Per\-formed by the Inmates +of the Asylum of Charenton Under the Direc\-tion of the +Marquis de~Sade!} But I {\em did} see it. +\end{minipage}\\ +In the nested emphasis, \cs{emph} had to be given for each word separately +so the spaces between could stretch and break into lines. Even the +discretionary hyphen (|\-|) in `Assassination' had to be outside the braces, +but the hyphen in `Direction' was just fine because it was not in nested +braces. The same applies to other special commands like |\ | and |~|. Also, +the spaces are printed with only a single underline because they are +outside the nested \cs{emph} commands. This example really illustrates that +ulem does not handle nested emphasis very well! It should be reserved for +simpler cases where it performs well without effort. + +\end{document} diff --git a/tesi/ulem.sty b/tesi/ulem.sty new file mode 100644 index 0000000..85ebb06 --- /dev/null +++ b/tesi/ulem.sty @@ -0,0 +1,376 @@ +% +% U L E M . S T Y [2019-11-18] +% +% The ulem package provides various types of underlining that can stretch +% between words and be broken across lines in LaTeX or plain TeX. +% In LaTeX ulem replaces italics with underlining in \em-phasized text. +% It is most suitable for simple text such as {\em ibid.} or \emph{\LaTeX: +% A Document Preparation System} that may need to be underlined in a +% manuscript submitted for publication. A declaration of \normalem (or +% the \usepackage option "normalem") restores the normal \em behavior. +% +% Full instructions appear in ulem.ltx (ulem.pdf). In summary: +% +% \uline{important} underlined text +% \uuline{urgent} double-underlined text +% \uwave{boat} wavy underline +% \sout{wrong} line drawn through word +% \xout{removed} marked over with //////. +% \dashuline{dashing} dash underline +% \dotuline{dotty} dotted underline +% +% {\em phasized\/} | In LaTeX, by default, these are underlined; use +% \emph{asized} | \normalem or [normalem] to restore italics +% \useunder{\uwave}{\bf}{\textbf} +% use wavy underline in place of bold face +% Use \markoverwith for defining new types of underlining. +% +% Copyright (c) 1989-2011 by Donald Arseneau (Vancouver, Canada; asnd@triumf.ca) +% +% This software may be freely transmitted, reproduced, or modified for any +% purpose provided that this copyright notice is left intact. +% (Small excerpts may be taken and used without any restriction.) +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Defend against multiple loading. +\expandafter \ifx \csname UL@box\endcsname \relax \else + \immediate\write16{ulem.sty refuses to load twice. }\endinput \fi + +% Set catcode of @ in case it isn't a "letter" already +\chardef\ULthickness\catcode\string`\@ % hold catcode temporarily +\catcode\string`\@=11 + +% \UL@protected = \protected, if available, else \relax + +\begingroup +\global\expandafter\let\expandafter\UL@protected\csname protected\endcsname +\endgroup + +\UL@protected\def\uline{\relax \ifmmode\expandafter\underline + \else \bgroup\expandafter\ULset\fi} + +\newbox\UL@box +\newbox\UL@hyphenbox +\newskip\UL@skip +\newtoks\UL@hook +\newdimen\UL@height \UL@height=\maxdimen % flags being unused +\newcount\UL@pe + +\UL@protected\def\UL@end *{\relax\relax}% something harmless but unique + +% For regular underlines, set the depth based on the font, or retain +% the preset value, then start underlining. +\def\ULset{\UL@setULdepth + \def\UL@leadtype{\leaders \hrule \@height\UL@height \@depth\ULdepth}% + \ifmmode \ULdepth-4\p@ \fi + \UL@height-\ULdepth \advance\UL@height\ULthickness \ULon} + +% Automatically set \ULdepth if it is to be automatic (flagged by \maxdimen) +\def\UL@setULdepth{\relax + \ifdim\ULdepth=\maxdimen % Set depth based on font, if not set already + \setbox\UL@box\hbox{{(j}}\ULdepth\dp\UL@box\advance\ULdepth.4\p@ + % use setbox to support plain TeX + \fi} + +% \ULon simply calls \UL@on (possibly \UL@on=\UL@onin) for text mode, but +% \UL@onmath if it is math mode. +\def\ULon{\ifmmode \expandafter\UL@onmath\else \expandafter\UL@on\fi} + +% \UL@on sets the engine of underline running, and tells it +% where to stop. #1 = the relevant text. +\long\def\UL@on#1{\leavevmode\UL@ender \let\UL@on\UL@onin + \everymath{\UL@hrest}\everyvbox{\UL@hrest}\let\hskip\UL@hskip + \let\\\UL@cr \let\-\UL@dischyp \let\newline\UL@newline \let\ \UL@space + \def\hfil{\hskip\z@ plus1fil\relax}\def\hfill{\hskip\z@ plus1fill\relax}% + \def\hss{\hskip\z@ plus1filminus1fil\relax}\let\penalty\UL@penalty + \the\UL@hook + \UL@word\@empty#1\xdef\UL@spfactor{\the\spacefactor} \UL@end * } + +% This is what \ULon does when it appears nested in an inner place. +\long\def\UL@onin#1{\leavevmode\UL@ender % when nested, do multiple underlining + \ifdim\ULdepth=\maxdimen\else + \UL@height\ULthickness \advance\ULdepth\thr@@\UL@height \advance\UL@height-\ULdepth + \fi + \setbox\UL@box\hbox{{#1}}% + \let\UL@start\relax\UL@putbox\egroup} +% \UL@putbox is disabled in inner mode, so re-enable it by changing \UL@start +% \UL@hrest is implicit due to \everyhbox. Double braces for \hbox are in +% lieu of \color@begin(end)group. + +% This is what \ULon does in math mode. +\def\UL@onmath#1{\UL@ender\mathord{\UL@hrest\mathop{\kern\z@#1}\limits\sb + {\UL@leadtype\LA@hskip\p@ plus1fill}}\egroup} + +\def\UL@unegroup{} +\gdef\UL@ender{} +% end-brace matching hack for when command is used as a font declaration: +\def\UL@swender{\ifnum`{=\z@\fi\aftergroup}\gdef\UL@ender{}} + +% must expand to nothing outside the ifs for syntactical spaces to work. +% the \expandafters get rid of the \@empty inserted at the beg. of word +\long\def\UL@word#1 {\expandafter\UL@start#1 % + \expandafter\ifx\expandafter\UL@end#1\egroup\egroup + \unskip \unskip \unskip % remove extra leader at end + \spacefactor\UL@spfactor \let\UL@word\egroup + \else % not finished + \ifmmode\else \ifdim\lastskip=\z@\else % allow syntactical spaces + \global\UL@skip\lastskip \unskip + \UL@stop \UL@leaders + \fi\fi + \fi \UL@word\@empty}% \@empty preserves braces in param + +% \UL@start: start of each chunk. It gives two levels of grouping. +% Each chunk is ended by \UL@stop. Local intermissions go like +% \UL@stop...\UL@start. +\def\UL@start{\setbox\UL@box\hbox\bgroup\everyhbox{\UL@hrest}% +% the following are to cope with stops (\ ,\- etc) within extra braces + \let\UL@start\@empty \def\UL@unegroup{\bgroup\bgroup}\let\UL@leadtype\@empty + \bgroup \kern-3sp\kern3sp % kerns so I can test for beginning of list + \if@ignore \global\@ignorefalse \ignorespaces \fi} + +\def\UL@stop{\global\UL@pe\lastpenalty \unpenalty % penalty in \UL@pe + \ifnum\lastkern=\thr@@ \egroup\egroup % Nothing in hbox...but make sure: + \ifdim\wd\UL@box=\z@ \else \UL@putbox \fi % something in box so print it + \else \egroup\egroup \UL@putbox % something in box so print it + \fi \ifnum\UL@pe=\z@ \else \LA@penalty\UL@pe \fi % use penalty from inside box + \UL@unegroup} +% notice that a box with only a penalty in it is discarded, but the penalty +% is still used! This is so a series of discardable glues and penalties +% behaves properly. + +\def\UL@putbox{\ifx\UL@start\@empty \else % not inner + \vrule\@width\z@ \LA@penalty\@M + {\UL@skip\wd\UL@box \UL@leaders \kern-\UL@skip}% + \box\UL@box + \fi} + +% With interword leaders, give some overlap to avoid gaps caused by +% round-off errors in the printing program. Needs \unskip \unskip \unskip +% above. This version overlaps 1/300 inch, which looks good at high +% resolution, and will still work down to ~150 dpi. Change the value +% of \UL@pixel if necessary. + +\newdimen\UL@pixel \UL@pixel=1in \divide\UL@pixel 300 + +\def\UL@leaders{{\LA@hskip-\UL@pixel \advance\UL@skip\tw@\UL@pixel + \UL@leadtype\LA@hskip\UL@skip \LA@hskip-\UL@pixel}} + +% restore some things for inside math or \mbox +\def\UL@hrest{\let\ \LA@space \let\-\@empty \let\penalty\LA@penalty} + +\let\LA@space\ % +\UL@protected\def\UL@space{\LA@space \global\UL@skip\lastskip \unskip \UL@reskip}% + +% Hyphenation is done by explicit \discretionary. The overlapping melds +% with the running overlap because it *is* part of the running overlap: +% The word fragment is extended by the width of the hyphenation which is +% then overlapped by leaders. The discretionary may occupy this space +% if a break occurs; otherwise the next syllable gets doubly-overlapped +% (in registration) for a distance of the hyphen's width. +\UL@protected\def\UL@dischyp{\global\setbox\UL@hyphenbox\hbox + {\ifnum \hyphenchar\font<\z@ \string-\else \char\hyphenchar\font \fi}% + \kern\wd\UL@hyphenbox \LA@penalty\@M + \UL@stop \kern-\wd\UL@hyphenbox + \discretionary{\box\UL@hyphenbox}{}{}\UL@start} + +\let\LA@penalty\penalty +\UL@protected\def\UL@penalty{\relax\ifhmode \afterassignment\UL@@penalty\count@ + \else\LA@penalty\fi} +\def\UL@@penalty{\LA@penalty \ifnum\count@=\z@ + \@ne \else \count@ \fi % zero penalty => no penalty, so use 1 instead. + \UL@stop \UL@start} + +% The test \ifx\ \LA@space \else means we are neither in math mode nor an +% \mbox, so it is safe to stop the current \UL@box. \ , \- , and \penalty +% (= \linebreak or \nolinebreak) are common enough that they are restored +% directly (by \UL@hrest); \\, \newline, \hskip (= \hspace) are rare enough +% that the test is incorporated in their UL versions. This adds processing +% when they're used, but saves processing in \UL@hrest called by \everymath +% \everyvbox and \everyhbox. + +\let\LA@hskip\hskip +\UL@protected\def\UL@hskip{\ifx\ \LA@space \LA@hskip \else + \afterassignment\UL@reskip \global\UL@skip \fi} + +\def\UL@reskip{\UL@stop \UL@leaders \UL@start} + +% Redefine \\ and \newline so the vertical space from \\[ ] is not lost +% and so the \hfil is not underlined! \\ and \newline do nothing if inside +% inner braces. + +\UL@protected\def\UL@cr{\unskip \ifx\ \LA@space \let\UL@vad\@gobble + \else \UL@stop \unskip\unskip\unskip \let\UL@vad\vadjust \fi + \@ifstar{\UL@vad{\LA@penalty\@M}\UL@cra}\UL@cra} +\def\UL@cra{\@ifnextchar[\UL@crb\UL@newline} +\def\UL@crb[#1]{\UL@vad{\vskip#1}\UL@newline} + +\UL@protected\def\UL@newline{\ifx\UL@start\@empty % (\UL@cr may have \UL@stop-ed already) + \unskip \ifx\ \LA@space \else \UL@stop \unskip\unskip\unskip \fi\fi + \LA@hskip \z@\@plus.0001fil\LA@penalty -\@M \UL@start} + +% That concludes the basic underlining. To put various other objects +% (characters) under (or over) text we need to define \markoverwith +% to set the overlay material in a box, and use leaders of that box for +% overlaying the text. Here, the meaning of \UL@pixel is changed so +% that `pixel' size = box size. Note that we generally need \leaders +% (not \cleaders) for text, because an underline will be a patchwork +% of small \leaders, and the characters must stay in registration. +% However, we "hook" the leaders command so specific applications can +% reassign it (\let\ULleaders\xleaders or \let\ULleaders\cleaders). +% +\newbox\ULC@box +\let\ULleaders\leaders + +\UL@protected\def\markoverwith#1{\leavevmode + \setbox\ULC@box\hbox{{#1}}\UL@pixel.5\wd\ULC@box + \ifmmode \setbox\ULC@box\hbox{\raise1.4ex\box\ULC@box}% + \dp\ULC@box-1.4ex\ht\ULC@box\z@ \def\UL@leadtype{\cleaders\copy\ULC@box}% + \else + \def\UL@leadtype{\ULleaders\copy\ULC@box}% + \fi} + +% Now define various special underlines. All the definitions go like +% \def \command {\bgroup \markoverwith{something} \ULon} + +% For drawing a wavey underline instead of a straight one the command +% is \uwave (under-wave) which uses the wiggle from 6-pt lasy font: + +\UL@protected\def\uwave{\leavevmode \bgroup + \ifdim \ULdepth=\maxdimen \ULdepth 3.5\p@ + \else \advance\ULdepth2\p@ + \fi \markoverwith{\lower\ULdepth\hbox{\sixly \char58}}\ULon} +\font\sixly=lasy6 % does not re-load if already loaded, so no memory drain. + +% To draw a double underline under text, use \uuline{text} + +\UL@protected\def\uuline{\leavevmode \bgroup + \UL@setULdepth + \ifx\UL@on\UL@onin \advance\ULdepth2.8\p@\fi + \markoverwith{\lower\ULdepth\hbox + {\kern-.03em\vbox{\hrule width.2em\kern1\p@\hrule}\kern-.03em}}% + \ULon} + +% To draw a line through text instead of under it (strike out) do +% `under'-line with negative depth. Note that this one uses a real +% line, not characters, so there is no \markoverwith. + +\UL@protected\def\sout{\leavevmode \bgroup \ULdepth=-.55ex \ULset} + +% To mark //// over text instead of underlining (x-out) +% +\UL@protected\def\xout{\leavevmode \bgroup + \markoverwith{\hbox to.35em{\hss/\hss}}\ULon} + +\UL@protected\def\dotuline{\leavevmode \bgroup + \UL@setULdepth + \ifx\UL@on\UL@onin \advance\ULdepth2\p@\fi + \markoverwith{\begingroup + %\advance\ULdepth0.08ex + \lower\ULdepth\hbox{\kern.06em .\kern.04em}% + \endgroup}% + \ULon} + +\UL@protected\def\dashuline{\leavevmode \bgroup + \UL@setULdepth + \ifx\UL@on\UL@onin \advance\ULdepth2\p@\fi + \markoverwith{\kern.13em + \vtop{\kern\ULdepth \hrule width .3em}% + \kern.13em}\ULon} + +% A command to declare that an underline command should be used in +% place of a particular font selection: +% \useunder {underline_command}{font_declaration}{font_command} +% e.g.: \useunder{\uuline}{\bfseries}{\textbf} +% \useunder{\uwave}{\bf}{} + +\UL@protected\def\useunder#1#2#3{\relax + \ifx\relax#2\relax\else % declaration command given + \UL@protected\def#2{\def\@tempa{#1}\global\let\UL@ender\UL@swender + \expandafter\@tempa\expandafter{\ifnum\z@=\string`}\fi}% + \fi + \ifx\relax#3\relax\else % argumentative command + \UL@protected\def#3{#1}% + \fi} + +\expandafter\ifx \csname @ifundefined\endcsname \relax + +% Allow plain TeX to use ulem.sty: + \def\@height{height} + \def\@depth{depth} + \def\@width{width} + \def\@empty{} + \long\def\@gobble#1{} + \long\def\@firstoftwo#1#2{#1}% + \long\def\@secondoftwo#1#2{#2}% +% Do non-outer \newif with no visible \if's or \fi's when skipping + \csname newif\expandafter\endcsname \csname if@ignore\endcsname + +\else + + \let\LA@em\em \let\LA@emph\emph + \expandafter\let\expandafter\LA@Pem \csname em \endcsname + \expandafter\let\expandafter\LA@Pemph \csname emph \endcsname + \def\ULforem{\useunder{\uline}{\em}{\emph}} + \def\normalem{\let\em\LA@em \let\emph\LA@emph + \expandafter\let\csname em \endcsname\LA@Pem + \expandafter\let\csname emph \endcsname\LA@Pemph} + \ULforem % default is to use underlining for \em, + +\fi + +% Process LaTeX \package options; plain TeX skips this section + +\expandafter\ifx\csname ProvidesPackage\endcsname \relax \else + \ProvidesPackage{ulem}[2019/11/18] + \DeclareOption{normalem}{\normalem} + \DeclareOption{ULforem}{\ULforem} + \DeclareOption{normalbf}{} + \DeclareOption{UWforbf}{\useunder{\uwave}{\bf}{\textbf}} + \ProcessOptions +% + \newcommand\UL@marpar[2][\ULmp@opt@arg]{\gdef\ULmp@opt@arg{#2}% + \ifx\ \LA@space \@latexerr{Marginpar lost}% + \else \UL@stop \LA@marginpar[#1]{#2}\UL@start \fi} +% + \AtBeginDocument{\let\LA@marginpar\marginpar}% +% + \addto@hook\UL@hook{\let\marginpar\UL@marpar} +\fi + +\catcode`@=\ULthickness % Scratch meaning: restore catcode of @ + +\def\ULthickness{.4pt}% can change this with \renewcommand +\newdimen\ULdepth \ULdepth=\maxdimen +% "maxdimen" depth causes the depth to be set according to the font. You +% can change \ULdepth for a permanent setting or a special effect (\sout). + +\endinput + + +% Previous bug-finders: Esther Hu (\hfill in plain); Lones Smith (\tt\-); +% Steve Anderson (\ooalign accents); Thanassi Protopapas ( { in tables). +% The bug finders' fee is now $0.00; it will double for each new bug found. +% Version (identified by year) +% 1994: +% Many changes! Notably: LaTeX2e options and \emph. Nesting works (somewhat). +% Behavior with inner braces is more consistent (not stripped). \useunder. +% Better underwave (using lasy6). Special underlines are not commented out. +% patch 1995: fix \UL@swender to work in {tabular}; make hyphenation join +% well; crude math support; eliminate \@clb +% 1996: use "\csname ProvidesPackage\endcsname", tidying. +% 1997: fix \\ when LaTeX changed; remove extra overlap in putbox. +% 2000: hook (and marginpar) +% 2004: Fix spacing in \uwave and \xout. \ULleaders hook. +% 2009: Accept \par in argument (\long) +% 2010: Include \dotuline and \dashuline, typeset documentation, add \UL@setULdepth +% 2011: Change \dimen@ to \UL@height +% 2012: Removed \let\par garbage +% 2017: Remove \makerobust +% 2019: Handle \ULdepth better. Some tweaks. +% +% Send problem reports to asnd@triumf.ca +% +% test integrity: +% brackets: round, square, curly, angle: () [] {} <> +% backslash, slash, vertical, at, dollar, and: \ / | @ $ & +% hat, grave, acute (apostrophe), quote, tilde, under: ^ ` ' " ~ _