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 it secret.


	Makarius




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