On 30/06/17 16:39, Manuel Eberl wrote: > > The advantage of qualified names is that they really allow us to add > disambiguating context to ambiguous names when necessary, e.g. something > like "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I > do understand that typing such lengthy names is tedious.
Just for typing it there is semantic completion in the Prover IDE. For constants in the term language, it requires trailing "_" to say that it is really meant to be a constant and not a variable. To actually complete such long name components as "subseq" in "Topological_Spaces.subseq", I have now made a tiny change in Isabelle/f50e6e31a0ee. Also note that the completion history reorders frequently used completions later on, so the long list of completion items becomes practically usable. > Incidentally, I wonder if it is possible to locally prefer one of the > two constants, i.e. say that, in the following block, I want "subseq" to > mean "Topological_Spaces.subseq". That might also mitigate the problem > of long qualified names. That introduces some extra complexity in the theory source, apart from input methods. Nonetheless, the 'alias' command from Isabelle/df85956228c2 can in principle do that: it merely exposes an important Isabelle/ML interface from recent years as Isar command. I did not do this earlier, because aliases have the potential for extra confusion of names in a theory, but proper name space operations are better than simulating that with 'notation' / 'no_notation'. (Alphabetic syntax tokens should be kept at a minimum anyway: they are subtracted from the identifier syntax category.) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev