citation tooltip/hyperlink based on open buffers with .bib files;

--- a/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 17:58:36 2014 +0200
@@ -55,7 +55,7 @@
   val position_properties: string list
   val positionN: string val position: T
   val expressionN: string val expression: T
-  val citationN: string val citation: T
+  val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
   val indentN: string
@@ -349,7 +349,7 @@
 
 (* citation *)
 
-val (citationN, citation) = markup_elem "citation";
+val (citationN, citation) = markup_string "citation" nameN;
 
 
 (* external resources *)

--- a/src/Pure/PIDE/markup.scala	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Oct 05 17:58:36 2014 +0200
@@ -123,6 +123,7 @@
   /* citation */
 
   val CITATION = "citation"
+  val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */

--- a/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 17:58:36 2014 +0200
@@ -21,11 +21,13 @@
       (Scan.lift
         (Scan.option (Parse.verbatim || Parse.cartouche) --
          Scan.repeat1 (Parse.position Args.name)))
-      (fn {context = ctxt, ...} => fn (opt, cites) =>
+      (fn {context = ctxt, ...} => fn (opt, citations) =>
         let
-          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
+          val _ =
+            Context_Position.reports ctxt
+              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
-          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
+          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
         in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
 
 end;

--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 17:58:36 2014 +0200
@@ -9,6 +9,7 @@
 
 declare -a SOURCES=(
   "src/active.scala"
+  "src/bibtex_jedit.scala"
   "src/bibtex_token_markup.scala"
   "src/completion_popup.scala"
   "src/context_menu.scala"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 17:58:36 2014 +0200
@@ -0,0 +1,27 @@
+/*  Title:      Tools/jEdit/src/bibtex_jedit.scala
+    Author:     Makarius
+
+BibTeX support in Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.Buffer
+
+
+object Bibtex_JEdit
+{
+  /* buffer model entries */
+
+  def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
+    for {
+      buffer <- JEdit_Lib.jedit_buffers()
+      model <- PIDE.document_model(buffer).iterator
+      (name, offset) <- model.bibtex_entries.iterator
+    } yield (name, buffer, offset)
+}
+

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 17:58:36 2014 +0200
@@ -12,7 +12,7 @@
 
 import java.io.{File => JFile}
 
-import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.browser.VFSBrowser
 
 
@@ -136,6 +136,20 @@
     }
   }
 
+  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
+  {
+    GUI_Thread.require {}
+
+    push_position(view)
+
+    view.goToBuffer(buffer)
+    try { view.getTextArea.moveCaretPosition(offset) }
+    catch {
+      case _: ArrayIndexOutOfBoundsException =>
+      case _: IllegalArgumentException =>
+    }
+  }
+
   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
     GUI_Thread.require {}
@@ -186,6 +200,13 @@
       override def toString: String = "URL " + quote(name)
     }
 
+  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
+    new Hyperlink {
+      val external = false
+      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
+      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
+    }
+
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink {
       val external = false

--- a/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 16:05:17 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 17:58:36 2014 +0200
@@ -139,13 +139,13 @@
   private val language_elements = Markup.Elements(Markup.LANGUAGE)
 
   private val highlight_elements =
-    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+    Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR)
 
   private val hyperlink_elements =
-    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
 
   private val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
@@ -157,6 +157,7 @@
   private val tooltip_descriptions =
     Map(
       Markup.EXPRESSION -> "expression",
+      Markup.CITATION -> "citation",
       Markup.TOKEN_RANGE -> "inner syntax token",
       Markup.FREE -> "free variable",
       Markup.SKOLEM -> "skolem variable",
@@ -395,6 +396,13 @@
               }
             opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
+            val opt_link =
+              Bibtex_JEdit.entries_iterator.collectFirst(
+                { case (a, buffer, offset) if a == name =>
+                    PIDE.editor.hyperlink_buffer(buffer, offset) })
+            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
+
           case _ => None
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }