Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features

On 5/30/2012 1:29 PM, Makarius wrote:
On Wed, 30 May 2012, gottfried.barrow at wrote:

On 5/29/2012 2:29 AM, Lars Noschinski wrote:
On 26.05.2012 03:58, gottfried.barrow at wrote:
Being in the habit of using the Acrobat search is what messed me up. The
phrase "find_theorems" is listed in the index, but I had searched on
"find", and it didn't show up in the search, so I didn't even think
about the index.

Many PDF viewers choke on "fi", as generates an fi-ligature instead of two letters f and i.

I didn't know yet that Acrobat Reader could cause such extra problems. Which version is it?

I use Adobe Acrobat Pro X, which is the version that lets you edit the PDFs. When I do a search on "find" in isar-ref.pdf, only "Find" on page 221 is found. I get the same results with Adobe Reader X.

I did searches with two other PDF readers: STDU Viewer <>, and PDF-XChange Viewer <>.

The STDU Viewer search returns the same results as Adobe. The PDF-XChange Viewer search finds lots of "find", including "find theorems" for the command "find_theorems".

On page 30, I selected "finding" in the 3 PDF viewers and the 1 PDF editor mentioned above. I copied the text into a text file. Here's what I get:

?nding (PDF-XChange)
?nding (STDU Viewer)
nding (Adobe Reader X)
nding (Adobe Acrobat Pro X)

Which is not what I really got in the text editor. There were two non-"f" or non-"i" characters preceding "nding" for Adobe.

It appears it's as Lars says about the "fi", and PDF-XChange does some extra work to find the "fi" in a word, and Acrobat doesn't.


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