src/Tools/jEdit/src/bibtex_jedit.scala

--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun Oct 05 18:14:26 2014 +0200
@@ -10,12 +10,21 @@
 import isabelle._
 
 
+import javax.swing.text.Segment
+import javax.swing.tree.DefaultMutableTreeNode
+
 import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
+
+import sidekick.{SideKickParser, SideKickParsedData}
 
 
 object Bibtex_JEdit
 {
-  /* buffer model entries */
+  /** buffer model **/
+
+  def check(buffer: Buffer): Boolean =
+    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
 
   def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
     for {
@@ -23,5 +32,132 @@
       model <- PIDE.document_model(buffer).iterator
       (name, offset) <- model.bibtex_entries.iterator
     } yield (name, buffer, offset)
+
+
+
+  /** token markup **/
+
+  /* token style */
+
+  private def token_style(context: String, token: Bibtex.Token): Byte =
+    token.kind match {
+      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
+      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
+      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
+      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
+      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
+      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
+      case Bibtex.Token.Kind.IDENT =>
+        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
+        else
+          Bibtex.get_entry(context) match {
+            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
+            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
+            case _ => JEditToken.DIGIT
+          }
+      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
+      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
+      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
+    }
+
+
+  /* line context */
+
+  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
+
+  private class Line_Context(context: Option[Bibtex.Line_Context])
+    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
+
+
+  /* token marker */
+
+  class Token_Marker extends TokenMarker
+  {
+    override def markTokens(context: TokenMarker.LineContext,
+        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
+    {
+      val line_ctxt =
+        context match {
+          case c: Line_Context => c.context
+          case _ => Some(Bibtex.Ignored_Context)
+        }
+      val line = if (raw_line == null) new Segment else raw_line
+
+      val context1 =
+      {
+        val (styled_tokens, context1) =
+          line_ctxt match {
+            case Some(ctxt) =>
+              val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
+              val styled_tokens =
+                for { chunk <- chunks; tok <- chunk.tokens }
+                yield (token_style(chunk.kind, tok), tok.source)
+              (styled_tokens, new Line_Context(Some(ctxt1)))
+            case None =>
+              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+              (List(styled_token), new Line_Context(None))
+          }
+
+        var offset = 0
+        for ((style, token) <- styled_tokens) {
+          val length = token.length
+          val end_offset = offset + length
+
+          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
+            for (i <- offset until end_offset)
+              handler.handleToken(line, style, i, 1, context1)
+          }
+          else handler.handleToken(line, style, offset, length, context1)
+
+          offset += length
+        }
+        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+        context1
+      }
+      val context2 = context1.intern
+      handler.setLineContext(context2)
+      context2
+    }
+  }
+
+
+
+  /** Sidekick parser **/
+
+  class Sidekick_Parser extends SideKickParser("bibtex")
+  {
+    override def supportsCompletion = false
+
+    private class Asset(
+        label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
+      extends Isabelle_Sidekick.Asset(label, start, stop) {
+        override def getShortString: String = label_html
+        override def getLongString: String = source
+      }
+
+    def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
+    {
+      val data = Isabelle_Sidekick.root_data(buffer)
+
+      try {
+        var offset = 0
+        for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
+          val kind = chunk.kind
+          val name = chunk.name
+          val source = chunk.source
+          if (kind != "") {
+            val label = kind + (if (name == "") "" else " " + name)
+            val label_html =
+              "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
+            val asset = new Asset(label, label_html, offset, offset + source.size, source)
+            data.root.add(new DefaultMutableTreeNode(asset))
+          }
+          offset += source.size
+        }
+        data
+      }
+      catch { case ERROR(_) => null }
+    }
+  }
 }