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



On Wed, 30 May 2012, Lars Noschinski wrote:

[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

I've done investigations occasionally over the years -- it is an old and well-known problem, and still waiting for really good solutions.

My last attempt was stopped in winter 2011, see http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2012/doc-src/pdfsetup.sty with the critical \iffalse to disable the "experimental treatment of replacement text".

I had first started with cmap as recommended on the above stackexchange. One of the aspects mentioned in that thread is old OT1 vs. T1. I had other motivations than "fi" ligatures to use T1, but it did not work out for two reasons, IIRC: (1) conflict with the rail package for syntax diagrams, (2) lack of scalable cm fonts for T1.

Point (1) no longer applies, since @{rail} is now an Isabelle antiquotation (see the isar-ref manual for its documentation).

Point (2) -- status unknown. Maybe some improvements have emerged in the meantime.


in 2010/2011 I ended up trying something completely different, using "ActualText" markup for PDF. It essentially allows to define a plain text model for the rendered text. This is a nice idea, but most browsers still have problems with it. Trying it again just now with the above pdfsetup.sty and \ifpdf instead of \iffalse to activate the markup, it produces the following result for isar-ref.pdf of Isabelle2012: http://www4.in.tum.de/~wenzelm/test/isar-ref.pdf

Using latest Acrobat Reader 10.1.3 in Windows 7 on the Isar proof on page 10/11 and copy/pasting into Isabelle/jEdit works *almost*:

  + Isabelle symbols fine, but need to be decoded on target
  + hidden quotes around inner syntax fine, but sometimes odd extra spaces
  - indentation is lost
  - page header gets in the way
  - fi ligatures don't work, e.g. "finally"

Sumatra PDF 2.1 just ignores the ActualText markup, but is able to copy the "finally" correctly :-)

Over all these years there has been a tension of HTML vs. PDF. I originally preferred proof documents with proper typesetting and pagination, but this now gets in the way for fully formal online text.

My hope is that someone who really understands HTML4/CSS2 or HTML5/CSS3 could give some hints how to make high-quality rendering of formal documents like the Isabelle manuals, or any other Isabelle document
from applications.


	Makarius






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