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 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.


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