# HG changeset patch # User wenzelm # Date 1412524716 -7200 # Node ID 30b75b7958d62c074b9b76b0ca2473b3de9f1229 # Parent 340f130b3d383083747aeb23052e2a16431ec048 citation tooltip/hyperlink based on open buffers with .bib files; diff -r 340f130b3d38 -r 30b75b7958d6 src/Pure/PIDE/markup.ML --- 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 *) diff -r 340f130b3d38 -r 30b75b7958d6 src/Pure/PIDE/markup.scala --- 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 */ diff -r 340f130b3d38 -r 30b75b7958d6 src/Pure/Tools/bibtex.ML --- 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; diff -r 340f130b3d38 -r 30b75b7958d6 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 340f130b3d38 -r 30b75b7958d6 src/Tools/jEdit/src/bibtex_jedit.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) +} + diff -r 340f130b3d38 -r 30b75b7958d6 src/Tools/jEdit/src/jedit_editor.scala --- 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 diff -r 340f130b3d38 -r 30b75b7958d6 src/Tools/jEdit/src/rendering.scala --- 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 } }