Re: [isabelle] Feature request: Clickable types in find_consts
On Wed, 1 Jul 2015, Matthew Fernandez wrote:
find_consts nat (* <- NOT ctrl-clickable, though results are *)
Could this be made to work in future?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and