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



On 20/08/2014 13:32, Makarius wrote:
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 {*
  Object_Logic.atomize
  *}


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:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2014-RC4/src/Pure/ML/ml_compiler_polyml.ML#l15


As Makarius says, the IDE markup from ML code is handled entirely by the Poly/ML system. This has been developed piecemeal and there are some parts of the ML syntax that are handled better than others. I've now committed a change (commit 1956) to Poly/ML SVN which includes location information for type constructors. That should mean it will eventually make its way into Isabelle but that will be some way down the line.

David




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