Re: [isabelle-dev] text_fold
Am 10.02.2014 14:18, schrieb Makarius: On Mon, 25 Nov 2013, Dmitriy Traytel wrote: Am 23.11.2013 19:42, schrieb Makarius: On Mon, 28 Oct 2013, Dmitriy Traytel wrote: Concerning the error messages: at least you should always get strictly more information than without coercion inference (i.e. the error message of the standard type-inference will always come first, only then coercion inference will give additional hints). Of course, the additional information can be distracting---maybe it should be hidden in a popup or so). Concerning the popup or so you could experiment with Pretty.text_fold (although the fold will be always open by default in currently published Isabelle versions). The Isabelle Pretty module started out as implementation of Oppen-style pretty-printing by Larry Paulson, but it has acquired more and more logical markup facilities over the years (e.g. Pretty.markup, Pretty.paragraph, Pretty.item). The full potential of this is still unused. (Display of advanced markup requires a proper PIDE front-end.) Thanks for the hint. There result of my experiments are in the development repository (2bbcbf8cf47e). This thread that originated from isabelle-users is still somehow open, see also https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00183.html In Isabelle/35354009ca25 I have sorted out some misunterstandings about Markup and Pretty. Pretty.text_fold is fine if you assemble pretty trees, but having already formatted strings means you can't go through a pretty tree again: Pretty.str assumes an atomic argument. (There used to be a mostly forgotten ML naming convention, to use str for unformatting strings and string for formatted ones, cf. Pretty.str vs. Pretty.str_of vs. Pretty.string_of.) I see. Thanks for repairing this. The reason why that API mismatch was not immediately detected is that Isabelle/Scala does its own rendering of pretty trees, from the overall output produced by the prover. This occasionally hides Isabelle/ML programming mistakes concerning Pretty.T, until someone uses a historical Isabelle front-end, or does Isabelle latex pretty printing. Using Markup.text_fold and already formatted strings in 35354009ca25 makes the situation formally more correct, and simpler. What I can't test here are all the individual error messages, because I don't know how to provoke them. I've merely done a sanity check with the original example from https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00208.html There are (commented) test cases for some of them in ~~/src/HOL/ex/Coercion_Examples.thy . I've checked those now and they seem fine. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On Fri, 10 Jan 2014, Clemens Ballarin wrote: This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want to add special treatment for this. Currently we can only ensure that a locale is intact by visiting its context. It would be better if integrity checking could be done in an incremental fashion. But that would require much more sophistication. There is a more general problem behind this: re-initializing a locale context is quite expensive, but we traditionally do this at certain important checkpoints when processing locale expressions. For example, in AFP/JinjaThreads the time for defining some huge locales is dominated by that re-init phase for the imports, and later only few facts are actually required. Several minutes (hours?) could probably be saved by maintaining facts within the context in a lazy manner: the name space is strict, but its values are only produced on demand. I have no clear idea, though, how that would impact practical realiablity of locale expressions. Or is that actually an answer to the problem above: assuming that re-init is fast, it could be done more often to check the name space, but its transformed results remain unchecked. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] underscore in latex
Some notes on that notoriously difficult topic. Classically the T1
encoding allows to get some actual (searchable) underscore characters,
depending on fonts.
See also
changeset: 55295:3951ced4156c
user:blanchet
date:Mon Feb 03 17:55:50 2014 +0100
files: src/Doc/Datatypes/Datatypes.thy
src/Doc/Datatypes/document/root.tex src/Doc/Nitpick/document/root.tex
src/Doc/Sledgehammer/document/root.tex
description:
searchable underscores
When I spotted that recently, I first thought it would suffer from the
known problem of really ugly bitmap fonts (EC), but it doesn't. Recent
TeXlive installations aready include the cm-super scalable fonts for T1
encoding with actual Type1 fonts in the PDF.
So I followed the move for the manuals where I am directly responsible:
changeset: 55363:9d5aba2baa4c
user:wenzelm
date:Sun Feb 09 16:17:01 2014 +0100
files: lib/texinputs/isabelle.sty
src/Doc/IsarImplementation/document/root.tex
src/Doc/IsarRef/document/root.tex src/Doc/IsarRef/document/style.sty
src/Doc/System/document/root.tex
description:
yet another attempt at actual underscore;
enforce scalable fonts for T1 encoding;
changeset: 55364:50c9a0ab1436
user:wenzelm
date:Sun Feb 09 16:31:24 2014 +0100
files: src/Doc/IsarImplementation/document/root.tex
src/Doc/IsarRef/document/root.tex src/Doc/System/document/root.tex
description:
do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super
fonts, which also provide underscore for non-tt font;
This seems to be mostly fine: proper underscore both for tt font (e.g. for
@{verbatim} and @{file} antiquotations) and regular formal text, e.g.
@{text}, @{term} etc.
The snag is this: Debian/Ubuntu TeXLive somehow manages to mess up
cm-super. (Even Cygwin gets it right by default without further ado.)
We have already the situation that a proper Isabelle release needs to be
produced on Mac OS X (via Admin/Release/build), so the included PDFs
should be fine by default.
Since Linux is the bad guy of the year 2013, I leave that default for now,
until there are even better ideas.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
