src/Tools/jEdit/src/rendering.scala
changeset 58545 30b75b7958d6
parent 58464 5e7fc9974aba
child 58592 b0fff34d3247
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 16:05:17 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Oct 05 17:58:36 2014 +0200
     1.3 @@ -139,13 +139,13 @@
     1.4    private val language_elements = Markup.Elements(Markup.LANGUAGE)
     1.5  
     1.6    private val highlight_elements =
     1.7 -    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
     1.8 +    Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     1.9        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.10        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    1.11        Markup.VAR, Markup.TFREE, Markup.TVAR)
    1.12  
    1.13    private val hyperlink_elements =
    1.14 -    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.15 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
    1.16  
    1.17    private val active_elements =
    1.18      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.19 @@ -157,6 +157,7 @@
    1.20    private val tooltip_descriptions =
    1.21      Map(
    1.22        Markup.EXPRESSION -> "expression",
    1.23 +      Markup.CITATION -> "citation",
    1.24        Markup.TOKEN_RANGE -> "inner syntax token",
    1.25        Markup.FREE -> "free variable",
    1.26        Markup.SKOLEM -> "skolem variable",
    1.27 @@ -395,6 +396,13 @@
    1.28                }
    1.29              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.30  
    1.31 +          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
    1.32 +            val opt_link =
    1.33 +              Bibtex_JEdit.entries_iterator.collectFirst(
    1.34 +                { case (a, buffer, offset) if a == name =>
    1.35 +                    PIDE.editor.hyperlink_buffer(buffer, offset) })
    1.36 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.37 +
    1.38            case _ => None
    1.39          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
    1.40    }