[isabelle-dev] AFP/Shivers-CFA latex document problem

Makarius makarius at sketis.net
Fri Nov 19 20:38:39 CET 2010

On Fri, 19 Nov 2010, Brian Huffman wrote:

> http://isabelle.in.tum.de/repos/isabelle/rev/b646316f8b3c
> basic setup for literal replacement text in PDF, to support copy/paste
> of Isabelle symbols;
> The root.tex of the Shivers-CFA entry contains the following two lines:
> \usepackage[normalem]{ulem}
> \newcommand{\isactrlps}[1]{{\uline #1}}
> Here is the stripped-down version of the entry I used for testing:
> theory Computability
> imports Pure
> begin
> definition foo :: "'a => 'a" ("\<^ps>") where
>  "\<^ps>f == f"
> end

The underlined " is crashing here due to the extra markup that tells that 
it is a literal quote.

In the default setup, this is defined as follows:


I have also tried \DeclareRobustCommand but \uline still crashes.

This one seems to work:


Is there anything special about ulem.sty that is required here?

In any case, \<^ps> can only treat a single Isabelle symbol (letter etc.). 
If more text should be marked up reliably, it would have to be done via 
slightly more awkward \<^bps>...\<^eps> that act like parentheses in 
LaTeX (\bgroup ... \egroup or similar).


More information about the isabelle-dev mailing list