clean name as in ML Completion.make;
authorwenzelm
Thu, 03 Sep 2015 13:56:32 +0200
changeset 61100 4d9efd5004c8
parent 61099 64dcd8609962
child 61101 7b915ca69af1
clean name as in ML Completion.make;
src/Pure/General/completion.scala
src/Tools/jEdit/src/bibtex_jedit.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))
 
--- 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 =>