Re: [isabelle] 0::'a

Am 18/11/2013 12:12, schrieb Makarius:
> 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.

You may observe that I intentionally wrote "with jedit" (rather than, eg, "in
jedit"). The word "with" indicates a contextual dependence, just like in Isar.
Anybody on this mailing list will immediately deduce from my previous mention of
PG that I am talking about the user interface to Isabelle. This is known as
natural language. Luckily you had no problem to follow it, as the rest of your
email clearly shows.


> 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 this:
>   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.
>     Makarius

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