Re: [isabelle] Underscore vs Hyphen in Document Preparation



On Mon, 2 Dec 2013, Alfio Martini wrote:

Documents generated with Isabelle build tool
produce an hyphen instead of an underscore whenever the
later is used in identifiers and concrete syntax annotation.

I think this is (a bit) unfortunate as a  choice for a default definition.

After a brief inspection of the isabelle.sty file, I added the
following workaround to my prelude.tex file:

def\isacharunderscore{\mbox{\_}}%

It works, but it I wonder if this is the proper way.

A more standard way is to use the high-level macro \isabellestyle, e.g. \isabellestyle{literal} to get closer to what you write in the source text. You can also try one of the tt forms.

Any attempt to change defaults will cause a major bloodshed among seasoned users of the Isabelle document prepration system. It will disrupt existing documents that assume certain styles implicitly.


Note that the small dash for rendering underscore emerged in 1996 as a typographically correct way to represent the idea of separating parts of identifiers in mathematical text, without making it look like "code". Today the majority of people have given up the very idea of separation altogether andPreferToWriteInCamelCaseEvenThoughThatIsHardlyReadable.

O tempora o mores!


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.