Re: [isabelle] locales, including documentation & possible programming bugs

On Fri, 4 May 2012, Brian Huffman wrote:

I agree that the omission of quotation marks in our pdf documentation is misleading and confusing, especially for new users who naturally want to copy examples manually from the pdf into their theory files.

This is an old problem, but showing the quotes alone does not help. Most new users try to copy-paste mechanically, not manually, and then get disappointed by the approximative result. Quotes, underscores, special symbols etc. may all appear differently depending on the underlying LaTeX styles of the documents in question.

I can happily report that the new "Programming and Proving in Isabelle/HOL" tutorial in the upcoming Isabelle2012 release does show quotation marks in the examples.

Copy paste fails here, as anticipated.  E.g. page 8, middle:

  fun app :: "′a list ⇒ ′a list ⇒ ′a list" where "app Nil ys = ys" |
    "app (Cons x xs) ys = Cons x (app xs ys)"

The single quotes are not the ASCII ones, so Isabelle will choke on that input. Such things can be tweaking in the LaTeX setup, but it is a never-ending story.

I've once tried a systematic approach where the original Isabelle source is associated with the visual typesetting (whatever that is), and it almost worked. Unfortunately some PDF browsers had problems with this addition to the PDF format from a few years ago, especially Mac OS Preview and Windows Acrobat Reader. Evince/Poppler on Linux was the only platform that worked reliably when I did the experiment 1-2 years ago.


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