Re: [isabelle] Isabelle2014-RC1: Completion of qualified fact names



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:

 thm foo<Ctrl-B>

... 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 approach anymore.


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.


	Makarius


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