[isabelle] Completion for long names inserts quotes
I like to use completion for constant and theorem names. Unfortunately, if the theorem
completes to a long name (i.e., something of the form xxx.yyyy), then completion wraps
this in quotes. For example,
completes to "list.map_comp" when I press Ctrl-B. I would find list.map_comp without the
quotes better because they are actually not needed, but I can live with the quotes. The
quotes really get annoying when I use completion for constants inside terms. For example,
when I press Ctrl-B after the underscore in
lemma "monotone ord option.le_ f"
lemma "monotone ord "option.le_fun" f"
and now I have to manually remove the quotes again to avoid parse errors. Is there a way
to avoid the quotes for completion?
This archive was generated by a fusion of
Pipermail (Mailman edition) and