[isabelle] Completion for long names inserts quotes



Dear Makarius,

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,

  thm list.map_com

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"

I get

 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?

Andreas




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