[isabelle-dev] underscore in latex

[Makarius]

Some notes on that notoriously difficult topic.  Classically the T1 
encoding allows to get some actual (searchable) underscore characters, 
depending on fonts.

See also

changeset:   55295:3951ced4156c
user:        blanchet
date:        Mon Feb 03 17:55:50 2014 +0100
files:       src/Doc/Datatypes/Datatypes.thy 
src/Doc/Datatypes/document/root.tex src/Doc/Nitpick/document/root.tex 
src/Doc/Sledgehammer/document/root.tex
description:
searchable underscores


When I spotted that recently, I first thought it would suffer from the 
known problem of really ugly bitmap fonts ("EC"), but it doesn't.  Recent 
TeXlive installations aready include the cm-super scalable fonts for T1 
encoding with actual Type1 fonts in the PDF.

So I followed the move for the manuals where I am directly responsible:

changeset:   55363:9d5aba2baa4c
user:        wenzelm
date:        Sun Feb 09 16:17:01 2014 +0100
files:       lib/texinputs/isabelle.sty 
src/Doc/IsarImplementation/document/root.tex 
src/Doc/IsarRef/document/root.tex src/Doc/IsarRef/document/style.sty 
src/Doc/System/document/root.tex
description:
yet another attempt at actual underscore;
enforce scalable fonts for T1 encoding;

changeset:   55364:50c9a0ab1436
user:        wenzelm
date:        Sun Feb 09 16:31:24 2014 +0100
files:       src/Doc/IsarImplementation/document/root.tex 
src/Doc/IsarRef/document/root.tex src/Doc/System/document/root.tex
description:
do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super 
fonts, which also provide underscore for non-tt font;


This seems to be mostly fine: proper underscore both for tt font (e.g. for 
@{verbatim} and @{file} antiquotations) and regular formal text, e.g. 
@{text}, @{term} etc.

The snag is this: Debian/Ubuntu TeXLive somehow manages to mess up 
cm-super.  (Even Cygwin gets it right by default without further ado.)

We have already the situation that a proper Isabelle release needs to be 
produced on Mac OS X (via Admin/Release/build), so the included PDFs 
should be fine by default.

Since Linux is the bad guy of the year 2013, I leave that default for now, 
until there are even better ideas.


 	Makarius