citation tooltip/hyperlink based on open buffers with .bib files;
authorwenzelm
Sun Oct 05 17:58:36 2014 +0200 (2014-10-05 ago)
changeset 5854530b75b7958d6
parent 58544 340f130b3d38
child 58546 72e2b2a609c4
citation tooltip/hyperlink based on open buffers with .bib files;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/bibtex.ML
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 17:58:36 2014 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    val position_properties: string list
     1.5    val positionN: string val position: T
     1.6    val expressionN: string val expression: T
     1.7 -  val citationN: string val citation: T
     1.8 +  val citationN: string val citation: string -> T
     1.9    val pathN: string val path: string -> T
    1.10    val urlN: string val url: string -> T
    1.11    val indentN: string
    1.12 @@ -349,7 +349,7 @@
    1.13  
    1.14  (* citation *)
    1.15  
    1.16 -val (citationN, citation) = markup_elem "citation";
    1.17 +val (citationN, citation) = markup_string "citation" nameN;
    1.18  
    1.19  
    1.20  (* external resources *)
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun Oct 05 16:05:17 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun Oct 05 17:58:36 2014 +0200
     2.3 @@ -123,6 +123,7 @@
     2.4    /* citation */
     2.5  
     2.6    val CITATION = "citation"
     2.7 +  val Citation = new Markup_String(CITATION, NAME)
     2.8  
     2.9  
    2.10    /* embedded languages */
     3.1 --- a/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
     3.2 +++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 17:58:36 2014 +0200
     3.3 @@ -21,11 +21,13 @@
     3.4        (Scan.lift
     3.5          (Scan.option (Parse.verbatim || Parse.cartouche) --
     3.6           Scan.repeat1 (Parse.position Args.name)))
     3.7 -      (fn {context = ctxt, ...} => fn (opt, cites) =>
     3.8 +      (fn {context = ctxt, ...} => fn (opt, citations) =>
     3.9          let
    3.10 -          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
    3.11 +          val _ =
    3.12 +            Context_Position.reports ctxt
    3.13 +              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
    3.14            val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
    3.15 -          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
    3.16 +          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
    3.17          in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
    3.18  
    3.19  end;
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 16:05:17 2014 +0200
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 05 17:58:36 2014 +0200
     4.3 @@ -9,6 +9,7 @@
     4.4  
     4.5  declare -a SOURCES=(
     4.6    "src/active.scala"
     4.7 +  "src/bibtex_jedit.scala"
     4.8    "src/bibtex_token_markup.scala"
     4.9    "src/completion_popup.scala"
    4.10    "src/context_menu.scala"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 17:58:36 2014 +0200
     5.3 @@ -0,0 +1,27 @@
     5.4 +/*  Title:      Tools/jEdit/src/bibtex_jedit.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +BibTeX support in Isabelle/jEdit.
     5.8 +*/
     5.9 +
    5.10 +package isabelle.jedit
    5.11 +
    5.12 +
    5.13 +import isabelle._
    5.14 +
    5.15 +
    5.16 +import org.gjt.sp.jedit.Buffer
    5.17 +
    5.18 +
    5.19 +object Bibtex_JEdit
    5.20 +{
    5.21 +  /* buffer model entries */
    5.22 +
    5.23 +  def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
    5.24 +    for {
    5.25 +      buffer <- JEdit_Lib.jedit_buffers()
    5.26 +      model <- PIDE.document_model(buffer).iterator
    5.27 +      (name, offset) <- model.bibtex_entries.iterator
    5.28 +    } yield (name, buffer, offset)
    5.29 +}
    5.30 +
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 16:05:17 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 17:58:36 2014 +0200
     6.3 @@ -12,7 +12,7 @@
     6.4  
     6.5  import java.io.{File => JFile}
     6.6  
     6.7 -import org.gjt.sp.jedit.{jEdit, View}
     6.8 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
     6.9  import org.gjt.sp.jedit.browser.VFSBrowser
    6.10  
    6.11  
    6.12 @@ -136,6 +136,20 @@
    6.13      }
    6.14    }
    6.15  
    6.16 +  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
    6.17 +  {
    6.18 +    GUI_Thread.require {}
    6.19 +
    6.20 +    push_position(view)
    6.21 +
    6.22 +    view.goToBuffer(buffer)
    6.23 +    try { view.getTextArea.moveCaretPosition(offset) }
    6.24 +    catch {
    6.25 +      case _: ArrayIndexOutOfBoundsException =>
    6.26 +      case _: IllegalArgumentException =>
    6.27 +    }
    6.28 +  }
    6.29 +
    6.30    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    6.31    {
    6.32      GUI_Thread.require {}
    6.33 @@ -186,6 +200,13 @@
    6.34        override def toString: String = "URL " + quote(name)
    6.35      }
    6.36  
    6.37 +  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
    6.38 +    new Hyperlink {
    6.39 +      val external = false
    6.40 +      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
    6.41 +      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
    6.42 +    }
    6.43 +
    6.44    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    6.45      new Hyperlink {
    6.46        val external = false
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 16:05:17 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 17:58:36 2014 +0200
     7.3 @@ -139,13 +139,13 @@
     7.4    private val language_elements = Markup.Elements(Markup.LANGUAGE)
     7.5  
     7.6    private val highlight_elements =
     7.7 -    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
     7.8 +    Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     7.9        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    7.10        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    7.11        Markup.VAR, Markup.TFREE, Markup.TVAR)
    7.12  
    7.13    private val hyperlink_elements =
    7.14 -    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    7.15 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
    7.16  
    7.17    private val active_elements =
    7.18      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    7.19 @@ -157,6 +157,7 @@
    7.20    private val tooltip_descriptions =
    7.21      Map(
    7.22        Markup.EXPRESSION -> "expression",
    7.23 +      Markup.CITATION -> "citation",
    7.24        Markup.TOKEN_RANGE -> "inner syntax token",
    7.25        Markup.FREE -> "free variable",
    7.26        Markup.SKOLEM -> "skolem variable",
    7.27 @@ -395,6 +396,13 @@
    7.28                }
    7.29              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    7.30  
    7.31 +          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
    7.32 +            val opt_link =
    7.33 +              Bibtex_JEdit.entries_iterator.collectFirst(
    7.34 +                { case (a, buffer, offset) if a == name =>
    7.35 +                    PIDE.editor.hyperlink_buffer(buffer, offset) })
    7.36 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    7.37 +
    7.38            case _ => None
    7.39          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
    7.40    }