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