--- a/src/Pure/General/completion.scala Thu Sep 03 11:39:27 2015 +0200
+++ b/src/Pure/General/completion.scala Thu Sep 03 13:56:32 2015 +0200
@@ -135,6 +135,10 @@
/** semantic completion **/
+ def clean_name(s: String): Option[String] =
+ if (s == "" || s == "_") None
+ else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
+
def report_no_completion(pos: Position.T): String =
YXML.string_of_tree(Semantic.Info(pos, No_Completion))
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Thu Sep 03 11:39:27 2015 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Thu Sep 03 13:56:32 2015 +0200
@@ -79,10 +79,14 @@
{
for {
Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
+ name1 <- Completion.clean_name(name)
+
original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
- orig = Library.perhaps_unquote(original)
- entries = complete(name).filter(_ != orig)
+ original1 <- Completion.clean_name(Library.perhaps_unquote(original))
+
+ entries = complete(name1).filter(_ != original1)
if entries.nonEmpty
+
items =
entries.sorted.map({
case entry =>