Re: [isabelle] Isabelle2014-RC1: Completion of qualified fact names
- To: Lars Hupel <hupel at in.tum.de>
- Subject: Re: [isabelle] Isabelle2014-RC1: Completion of qualified fact names
- From: Makarius <makarius at sketis.net>
- Date: Fri, 1 Aug 2014 23:14:51 +0200 (CEST)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <53D9FB6D.firstname.lastname@example.org>
- References: <53D9FB6D.email@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 31 Jul 2014, Lars Hupel wrote:
assume this simple inductive definition:
inductive foo :: "nat ⇒ bool" where
foo1: "foo 0"
Now, trying the completion:
... this gives me "foo.cases", "foo.induct", ... (as expected), and also
"foo1". It doesn't give me "foo.foo1", though.
Peter suggested that the general policy seems to be that if the short
name is in scope, the longer name gets filtered out.
This corresponds to certain canonical ways to deal with internal vs.
external names in name spaces. The bahaviour comes out naturally without
further ado, and without rethinking the usual ways.
Could this be changed or configurable?
To do different one needs a clear counter-indication that the default is
not right. Lets say 2-3 convincing application scenarios. Configurable
"modes" are a measure of last resort, when there is no clear uniform
Side note: Pressing <Ctrl-B> after "thm foo." (notice the dot) doesn't
open the completion dialog.
The dot is a keyword and already complete on its own. If you want to
complete the name fragment "foo." you have to write it in quotes, and it
then gets correctly expanded without quotes.
This archive was generated by a fusion of
Pipermail (Mailman edition) and