# HG changeset patch
# User wenzelm
# Date 1441281392 -7200
# Node ID 4d9efd5004c8d090c9a4c9baec4e63514d615fa7
# Parent  64dcd860996235d75c8a32a9dd080008225cba6f
clean name as in ML Completion.make;

diff -r 64dcd8609962 -r 4d9efd5004c8 src/Pure/General/completion.scala
--- 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))
 
diff -r 64dcd8609962 -r 4d9efd5004c8 src/Tools/jEdit/src/bibtex_jedit.scala
--- 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 =>