Email Gateway (Aug 22 2022 at 10:36): Email Gateway (Aug 22 2022 at 10:36):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi,
I was wondering if I could be so bold as to request a minor convenience in future Isabelle.
Ctrl-click in Isabelle/jEdit allows you to jump to the definition of whatever is under the cursor,
but this doesn't seem to work in find_consts:
consts foo :: nat (* <- Ctrl-clickable *)
find_theorems "_::nat" (* <- Ctrl-clickable, also in results *)
find_consts nat (* <- NOT ctrl-clickable, though results are *)
Could this be made to work in future? If what I've asked for is unclear or unreasonable, please let
me know.
Thanks,
Matt
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:47):From: Makarius <makarius@sketis.net>
No problem. I am about to change that for the next release, although that
is still far ahead in the future.
The outer syntax parser for find_consts was using Parse.xname, but it
needs to be Parse.typ, to indicate that the parsed string is meant as a
type of the logic.
There might well be similar omissions in other tools. If anybody sees
anything like that, please report it publicly or privately, and don't keep
it secret.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC