src/Pure/Tools/bibtex.scala
changeset 66118 03dd799fe042
parent 64831 4792ee012e94
child 66150 c2e19b9e1398
equal deleted inserted replaced
66117:e6f808d1307c 66118:03dd799fe042
   420           error("Unepected failure to parse input:\n" + rest.source.toString)
   420           error("Unepected failure to parse input:\n" + rest.source.toString)
   421       }
   421       }
   422     }
   422     }
   423     (chunks.toList, ctxt)
   423     (chunks.toList, ctxt)
   424   }
   424   }
       
   425 
       
   426 
       
   427   /* completion */
       
   428 
       
   429   def completion(history: Completion.History, rendering: Rendering, caret: Text.Offset,
       
   430     complete: String => List[String]): Option[Completion.Result] =
       
   431   {
       
   432     for {
       
   433       Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
       
   434       name1 <- Completion.clean_name(name)
       
   435 
       
   436       original <- rendering.model.try_get_text(r)
       
   437       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
       
   438 
       
   439       entries = complete(name1).filter(_ != original1)
       
   440       if entries.nonEmpty
       
   441 
       
   442       items =
       
   443         entries.sorted.map({
       
   444           case entry =>
       
   445             val full_name = Long_Name.qualify(Markup.CITATION, entry)
       
   446             val description = List(entry, "(BibTeX entry)")
       
   447             val replacement = quote(entry)
       
   448           Completion.Item(r, original, full_name, description, replacement, 0, false)
       
   449         }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
       
   450     } yield Completion.Result(r, original, false, items)
       
   451   }
   425 }
   452 }