[isabelle] Feature request: Clickable types in find_consts



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.




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