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



On 30.05.2012 18:35, gottfried.barrow at gmx.com wrote:
On 5/29/2012 2:29 AM, Lars Noschinski wrote:
On 26.05.2012 03:58, gottfried.barrow at gmx.com 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.

[...] as [LaTeX] generates [...]

However, it never occurred to me that "fi" in a word would cause
problems with Acrobat search. Now I know. Thanks, because Acrobat search
is useful if I know its limitations.

[1] suggests that this problem can be solved at document generation time. Maybe this is worth investigating.

[1] http://tex.stackexchange.com/questions/33476/why-cant-fi-be-separated-when-being-copied-from-a-compiled-pdf

 -- Lars





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