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

[Makarius]

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:

   \newcommand{\isaliteral}[2]{#2}

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

This one seems to work:

   \newcommand{\isactrlps}[1]{\underline{#1}}


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).


 	Makarius