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