--- a/NEWS Mon Oct 06 14:21:38 2014 +0200
+++ b/NEWS Mon Oct 06 16:54:35 2014 +0200
@@ -22,7 +22,7 @@
* Document antiquotation @{cite} provides formal markup, which is
interpreted semi-formally based on .bib files that happen to be opened
-in the editor (hyperlinks etc.).
+in the editor (hyperlinks, completion etc.).
*** Pure ***
--- a/src/Pure/library.scala Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Pure/library.scala Mon Oct 06 16:54:35 2014 +0200
@@ -145,6 +145,8 @@
if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
else None
+ def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
+
def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Mon Oct 06 16:54:35 2014 +0200
@@ -29,9 +29,14 @@
{
/** buffer model **/
+ /* file type */
+
def check(buffer: Buffer): Boolean =
JEdit_Lib.buffer_name(buffer).endsWith(".bib")
+
+ /* parse entries */
+
def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] =
{
val chunks =
@@ -47,6 +52,9 @@
result.toList
}
+
+ /* retrieve entries */
+
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
for {
buffer <- JEdit_Lib.jedit_buffers()
@@ -55,6 +63,38 @@
} yield (name, buffer, offset)
+ /* completion */
+
+ def complete(name: String): List[String] =
+ {
+ val name1 = name.toLowerCase
+ (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1))
+ yield entry).toList
+ }
+
+ def completion(
+ history: Completion.History,
+ text_area: JEditTextArea,
+ rendering: Rendering): Option[Completion.Result] =
+ {
+ for {
+ Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
+ original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
+ orig = Library.perhaps_unquote(original)
+ entries = complete(name).filter(_ != orig)
+ if !entries.isEmpty
+ items =
+ entries.map({
+ case entry =>
+ val full_name = Long_Name.qualify(Markup.CITATION, entry)
+ val description = List(entry, "(BibTeX entry)")
+ val replacement = quote(entry)
+ Completion.Item(r, original, full_name, description, replacement, 0, false)
+ }).sorted(history.ordering).take(PIDE.options.int("completion_limit"))
+ } yield Completion.Result(r, original, false, items)
+ }
+
+
/** context menu **/
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Oct 06 16:54:35 2014 +0200
@@ -134,7 +134,10 @@
case None =>
Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, false, Some(rendering)),
- path_completion(rendering)).map(_.range)
+ Completion.Result.merge(Completion.History.empty,
+ path_completion(rendering),
+ Bibtex_JEdit.completion(Completion.History.empty, text_area, rendering)))
+ .map(_.range)
}
case _ => None
}
@@ -380,7 +383,9 @@
Completion.Result.merge(history, result0,
Completion.Result.merge(history,
Spell_Checker.completion(text_area, explicit, rendering),
- path_completion(rendering)))
+ Completion.Result.merge(history,
+ path_completion(rendering),
+ Bibtex_JEdit.completion(history, text_area, rendering))))
}
}
result match {
--- a/src/Tools/jEdit/src/rendering.scala Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon Oct 06 16:54:35 2014 +0200
@@ -138,6 +138,8 @@
private val language_elements = Markup.Elements(Markup.LANGUAGE)
+ private val citation_elements = Markup.Elements(Markup.CITATION)
+
private val highlight_elements =
Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -296,6 +298,14 @@
case _ => None
}).headOption.map(_.info)
+ def citation(range: Text.Range): Option[Text.Info[String]] =
+ snapshot.select(range, Rendering.citation_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
+ Some(Text.Info(snapshot.convert(info_range), name))
+ case _ => None
+ }).headOption.map(_.info)
+
/* spell checker */