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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
