src/Tools/jEdit/src/bibtex_jedit.scala
author wenzelm
Sun Oct 05 18:14:26 2014 +0200 (2014-10-05 ago)
changeset 58546 72e2b2a609c4
parent 58545 30b75b7958d6
child 58547 6080615b8b96
permissions -rw-r--r--
clarified modules;
     1 /*  Title:      Tools/jEdit/src/bibtex_jedit.scala
     2     Author:     Makarius
     3 
     4 BibTeX support in Isabelle/jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import javax.swing.text.Segment
    14 import javax.swing.tree.DefaultMutableTreeNode
    15 
    16 import org.gjt.sp.jedit.Buffer
    17 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
    18 
    19 import sidekick.{SideKickParser, SideKickParsedData}
    20 
    21 
    22 object Bibtex_JEdit
    23 {
    24   /** buffer model **/
    25 
    26   def check(buffer: Buffer): Boolean =
    27     JEdit_Lib.buffer_name(buffer).endsWith(".bib")
    28 
    29   def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
    30     for {
    31       buffer <- JEdit_Lib.jedit_buffers()
    32       model <- PIDE.document_model(buffer).iterator
    33       (name, offset) <- model.bibtex_entries.iterator
    34     } yield (name, buffer, offset)
    35 
    36 
    37 
    38   /** token markup **/
    39 
    40   /* token style */
    41 
    42   private def token_style(context: String, token: Bibtex.Token): Byte =
    43     token.kind match {
    44       case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
    45       case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
    46       case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
    47       case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
    48       case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
    49       case Bibtex.Token.Kind.NAME => JEditToken.LABEL
    50       case Bibtex.Token.Kind.IDENT =>
    51         if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
    52         else
    53           Bibtex.get_entry(context) match {
    54             case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
    55             case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
    56             case _ => JEditToken.DIGIT
    57           }
    58       case Bibtex.Token.Kind.SPACE => JEditToken.NULL
    59       case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
    60       case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
    61     }
    62 
    63 
    64   /* line context */
    65 
    66   private val context_rules = new ParserRuleSet("bibtex", "MAIN")
    67 
    68   private class Line_Context(context: Option[Bibtex.Line_Context])
    69     extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
    70 
    71 
    72   /* token marker */
    73 
    74   class Token_Marker extends TokenMarker
    75   {
    76     override def markTokens(context: TokenMarker.LineContext,
    77         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    78     {
    79       val line_ctxt =
    80         context match {
    81           case c: Line_Context => c.context
    82           case _ => Some(Bibtex.Ignored_Context)
    83         }
    84       val line = if (raw_line == null) new Segment else raw_line
    85 
    86       val context1 =
    87       {
    88         val (styled_tokens, context1) =
    89           line_ctxt match {
    90             case Some(ctxt) =>
    91               val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
    92               val styled_tokens =
    93                 for { chunk <- chunks; tok <- chunk.tokens }
    94                 yield (token_style(chunk.kind, tok), tok.source)
    95               (styled_tokens, new Line_Context(Some(ctxt1)))
    96             case None =>
    97               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    98               (List(styled_token), new Line_Context(None))
    99           }
   100 
   101         var offset = 0
   102         for ((style, token) <- styled_tokens) {
   103           val length = token.length
   104           val end_offset = offset + length
   105 
   106           if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
   107             for (i <- offset until end_offset)
   108               handler.handleToken(line, style, i, 1, context1)
   109           }
   110           else handler.handleToken(line, style, offset, length, context1)
   111 
   112           offset += length
   113         }
   114         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   115         context1
   116       }
   117       val context2 = context1.intern
   118       handler.setLineContext(context2)
   119       context2
   120     }
   121   }
   122 
   123 
   124 
   125   /** Sidekick parser **/
   126 
   127   class Sidekick_Parser extends SideKickParser("bibtex")
   128   {
   129     override def supportsCompletion = false
   130 
   131     private class Asset(
   132         label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
   133       extends Isabelle_Sidekick.Asset(label, start, stop) {
   134         override def getShortString: String = label_html
   135         override def getLongString: String = source
   136       }
   137 
   138     def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
   139     {
   140       val data = Isabelle_Sidekick.root_data(buffer)
   141 
   142       try {
   143         var offset = 0
   144         for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
   145           val kind = chunk.kind
   146           val name = chunk.name
   147           val source = chunk.source
   148           if (kind != "") {
   149             val label = kind + (if (name == "") "" else " " + name)
   150             val label_html =
   151               "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
   152             val asset = new Asset(label, label_html, offset, offset + source.size, source)
   153             data.root.add(new DefaultMutableTreeNode(asset))
   154           }
   155           offset += source.size
   156         }
   157         data
   158       }
   159       catch { case ERROR(_) => null }
   160     }
   161   }
   162 }
   163