Re: [isabelle] How to check type information in Isabelle/ML

On Wed, 20 Aug 2014, Lars Noschinski wrote:

On 18.08.2014 19:10, Wenda Li wrote:
Dear Isabelle experts,

I was wondering if there is an easy way to jump to the file where a
type in Isabelle/ML is defined. For example, from

  ML {*

we can know that the function Object_Logic.atomize is of type

  val it = fn: Proof.context -> conv

we can also jump to the definition file of Object_Logic.atomize by
CTRL+left click at the method name. However, what if I want to know
more about the type "conv", is there a quick way to jump to the file
where "conv" is declared or defined? An ideal way might be to
CTRL+left click at "conv", but it does not seem to work for now.

Such a feature would be nice (as well as the option to jump into a
structure, even if I don't know any exported function in the structure);
but to my knowledge, your best bet are the usual search features.

Search means hypersearch in jEdit, which I am using a lot together with regular expressions, also exploiting the uniform naming conventions of the main Isabelle sources.

In that particular case, though, the formal markup is available in the following input:

  ML ‹structure A = Conv›

C-hover over "Conv" above works as usual.  But it does not work here:

  ML ‹type a = conv›

The details of the Poly/ML IDE markup are up to David Matthews. I merely harvest that information for PIDE here:


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