[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Tjark Weber]

On Fri, 2010-12-17 at 15:58 +0100, Makarius wrote:
> This kind of error message would be outdated and misleading in a very 
> short time.  We also have an internal collection of jokes about packages 
> that were a bit too chatty, pretending to know what the user needs to do 
> in a certain situation. The principles of modularity, maintainability etc. 
> need to be applied to error messages, too.

Well, I agree that verbatim pointers into PDFs would quickly turn into a
maintenance nightmare.  They aren't particularly convenient for users
either.  They are merely a low-tech approach that's trivial to realize.

One could think about (tool support for) formally checked hyperlinks
from ML sources into LaTeX (and other) documents.

Or one could look into help authoring tools, to see whether they can be
used to create proper context-sensitive help.  (Perhaps Jasmin has some
experience.)  Does jEdit offer useful functionality?  But that would be
a major move.

Kind regards,
Tjark