Re: [isabelle] 0::'a
On Mon, 18 Nov 2013, Tobias Nipkow wrote:
In ProofGeneral, numerals of type 'a are explicitly flagged with their
type in the output. It is an incredibly useful little feature, not just
but in particular for novices. Which is why we introduced it.
I introduced that feature many years ago, and even the idea to make a
constraint as "inlined warning" to give it the proper syntactic context.
(An explicit warning message within syntax translations technically does
not work, even today, and even though I've seen this occasionally in other
syntax translations over the years.)
Any reason not to have it with jedit as well?
You mean Isabelle/jEdit, or rather the Isabelle/Scala document model
behind it; jEdit is just a plain text editor.
The reason why the constraint is not immediately visible in the output is
the much richer term markup introduced in Isabelle2013:
* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.
The old TTY / ProofGeneral behaviour can be recovered by something like
declare [[show_markup = false]]
but this also looses the benefit of constraints that can be retrieved as
tooltips on demand.
To make further progress, without looking back on old features, there are
two things in the pipeline for quite some time (and with some priority):
* Highlighting of places in terms where extra polymorphism is
introduced. (Users are more often confused about basic type-inference
than just the special case of 0, 1, etc.)
* Routine printing of terms with just the right amount of type/sort
constraints, such that the result is uniquely determined.
This archive was generated by a fusion of
Pipermail (Mailman edition) and