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


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. Adding another
inductive which introduces another "foo1" rule confirms that observation.

  inductive foo2 :: "nat ⇒ bool" where
  foo1: "foo2 0"

  thm foo<Ctrl-B>

... now has "foo.foo1", but not "foo2.foo1".

Could this be changed or configurable? Sometimes, it is preferable to
give the long names, even if the shorter ones are in scope.

Side note: Pressing <Ctrl-B> after "thm foo." (notice the dot) doesn't
open the completion dialog.


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