Email Gateway (Aug 19 2022 at 15:27): Email Gateway (Aug 19 2022 at 15:27):From: Wenda Li <wl302@cam.ac.uk>
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
*}
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.
Many thanks,
Wenda
Email Gateway (Aug 19 2022 at 15:29):From: Lars Noschinski <noschinl@in.tum.de>
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.
-- Lars
Email Gateway (Aug 19 2022 at 15:30):From: Makarius <makarius@sketis.net>
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:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2014-RC4/src/Pure/ML/ml_compiler_polyml.ML#l15
Makarius
Email Gateway (Aug 19 2022 at 15:31):From: David Matthews <dm@prolingua.co.uk>
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
Last updated: Apr 26 2024 at 16:20 UTC