src/Tools/jEdit/src/bibtex_jedit.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64831 4792ee012e94
child 66115 135bf45026ea
permissions -rw-r--r--
tuned signature;
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@58547
    13
import scala.collection.mutable
wenzelm@58547
    14
wenzelm@58548
    15
import java.awt.event.{ActionListener, ActionEvent}
wenzelm@58548
    16
wenzelm@58546
    17
import javax.swing.text.Segment
wenzelm@58546
    18
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@58548
    19
import javax.swing.{JMenu, JMenuItem}
wenzelm@58546
    20
wenzelm@58545
    21
import org.gjt.sp.jedit.Buffer
wenzelm@58548
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
wenzelm@58546
    23
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
wenzelm@58546
    24
wenzelm@58546
    25
import sidekick.{SideKickParser, SideKickParsedData}
wenzelm@58545
    26
wenzelm@58545
    27
wenzelm@58545
    28
object Bibtex_JEdit
wenzelm@58545
    29
{
wenzelm@64829
    30
  /** completion **/
wenzelm@58592
    31
wenzelm@58592
    32
  def complete(name: String): List[String] =
wenzelm@64829
    33
    (for {
wenzelm@64831
    34
      Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator()
wenzelm@64829
    35
      if entry.toLowerCase.containsSlice(name.toLowerCase)
wenzelm@64829
    36
    } yield entry).toList
wenzelm@58592
    37
wenzelm@58592
    38
  def completion(
wenzelm@58592
    39
    history: Completion.History,
wenzelm@58592
    40
    text_area: JEditTextArea,
wenzelm@64621
    41
    rendering: JEdit_Rendering): Option[Completion.Result] =
wenzelm@58592
    42
  {
wenzelm@58592
    43
    for {
wenzelm@58592
    44
      Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
wenzelm@61100
    45
      name1 <- Completion.clean_name(name)
wenzelm@61100
    46
wenzelm@58592
    47
      original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
wenzelm@61100
    48
      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
wenzelm@61100
    49
wenzelm@61100
    50
      entries = complete(name1).filter(_ != original1)
wenzelm@59319
    51
      if entries.nonEmpty
wenzelm@61100
    52
wenzelm@58592
    53
      items =
wenzelm@61099
    54
        entries.sorted.map({
wenzelm@58592
    55
          case entry =>
wenzelm@58592
    56
            val full_name = Long_Name.qualify(Markup.CITATION, entry)
wenzelm@58592
    57
            val description = List(entry, "(BibTeX entry)")
wenzelm@58592
    58
            val replacement = quote(entry)
wenzelm@58592
    59
          Completion.Item(r, original, full_name, description, replacement, 0, false)
wenzelm@58592
    60
        }).sorted(history.ordering).take(PIDE.options.int("completion_limit"))
wenzelm@58592
    61
    } yield Completion.Result(r, original, false, items)
wenzelm@58592
    62
  }
wenzelm@58592
    63
wenzelm@58592
    64
wenzelm@58546
    65
wenzelm@58548
    66
  /** context menu **/
wenzelm@58548
    67
wenzelm@58548
    68
  def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
wenzelm@58548
    69
  {
wenzelm@58548
    70
    text_area0 match {
wenzelm@58548
    71
      case text_area: TextArea =>
wenzelm@58548
    72
        text_area.getBuffer match {
wenzelm@58548
    73
          case buffer: Buffer
wenzelm@64828
    74
          if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
wenzelm@58548
    75
            val menu = new JMenu("BibTeX entries")
wenzelm@58548
    76
            for (entry <- Bibtex.entries) {
wenzelm@58548
    77
              val item = new JMenuItem(entry.kind)
wenzelm@58548
    78
              item.addActionListener(new ActionListener {
wenzelm@58548
    79
                def actionPerformed(evt: ActionEvent): Unit =
wenzelm@58548
    80
                  Isabelle.insert_line_padding(text_area, entry.template)
wenzelm@58548
    81
              })
wenzelm@58548
    82
              menu.add(item)
wenzelm@58548
    83
            }
wenzelm@58548
    84
            List(menu)
wenzelm@58548
    85
          case _ => Nil
wenzelm@58548
    86
        }
wenzelm@58548
    87
      case _ => Nil
wenzelm@58548
    88
    }
wenzelm@58548
    89
  }
wenzelm@58548
    90
wenzelm@58548
    91
wenzelm@58548
    92
wenzelm@58546
    93
  /** token markup **/
wenzelm@58546
    94
wenzelm@58546
    95
  /* token style */
wenzelm@58546
    96
wenzelm@58546
    97
  private def token_style(context: String, token: Bibtex.Token): Byte =
wenzelm@58546
    98
    token.kind match {
wenzelm@58546
    99
      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
wenzelm@58546
   100
      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
wenzelm@58546
   101
      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
wenzelm@58546
   102
      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
wenzelm@58546
   103
      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
wenzelm@58546
   104
      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
wenzelm@58546
   105
      case Bibtex.Token.Kind.IDENT =>
wenzelm@58546
   106
        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
wenzelm@58546
   107
        else
wenzelm@58546
   108
          Bibtex.get_entry(context) match {
wenzelm@58546
   109
            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
wenzelm@58546
   110
            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
wenzelm@58546
   111
            case _ => JEditToken.DIGIT
wenzelm@58546
   112
          }
wenzelm@58546
   113
      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
wenzelm@58546
   114
      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
wenzelm@58546
   115
      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
wenzelm@58546
   116
    }
wenzelm@58546
   117
wenzelm@58546
   118
wenzelm@58546
   119
  /* line context */
wenzelm@58546
   120
wenzelm@58546
   121
  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
wenzelm@58546
   122
wenzelm@58699
   123
  private class Line_Context(val context: Option[Bibtex.Line_Context])
wenzelm@58699
   124
    extends TokenMarker.LineContext(context_rules, null)
wenzelm@58699
   125
  {
wenzelm@58699
   126
    override def hashCode: Int = context.hashCode
wenzelm@58699
   127
    override def equals(that: Any): Boolean =
wenzelm@58699
   128
      that match {
wenzelm@58699
   129
        case other: Line_Context => context == other.context
wenzelm@58699
   130
        case _ => false
wenzelm@58699
   131
      }
wenzelm@58699
   132
  }
wenzelm@58546
   133
wenzelm@58546
   134
wenzelm@58546
   135
  /* token marker */
wenzelm@58546
   136
wenzelm@58546
   137
  class Token_Marker extends TokenMarker
wenzelm@58546
   138
  {
wenzelm@58546
   139
    override def markTokens(context: TokenMarker.LineContext,
wenzelm@58546
   140
        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
wenzelm@58546
   141
    {
wenzelm@58546
   142
      val line_ctxt =
wenzelm@58546
   143
        context match {
wenzelm@58546
   144
          case c: Line_Context => c.context
wenzelm@58589
   145
          case _ => Some(Bibtex.Ignored)
wenzelm@58546
   146
        }
wenzelm@58546
   147
      val line = if (raw_line == null) new Segment else raw_line
wenzelm@58546
   148
wenzelm@58595
   149
      def no_markup =
wenzelm@58595
   150
      {
wenzelm@58595
   151
        val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
wenzelm@58595
   152
        (List(styled_token), new Line_Context(None))
wenzelm@58595
   153
      }
wenzelm@58595
   154
wenzelm@58546
   155
      val context1 =
wenzelm@58546
   156
      {
wenzelm@58546
   157
        val (styled_tokens, context1) =
wenzelm@58546
   158
          line_ctxt match {
wenzelm@58546
   159
            case Some(ctxt) =>
wenzelm@58595
   160
              try {
wenzelm@58595
   161
                val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
wenzelm@58595
   162
                val styled_tokens =
wenzelm@58595
   163
                  for { chunk <- chunks; tok <- chunk.tokens }
wenzelm@58595
   164
                  yield (token_style(chunk.kind, tok), tok.source)
wenzelm@58595
   165
                (styled_tokens, new Line_Context(Some(ctxt1)))
wenzelm@58595
   166
              }
wenzelm@58595
   167
              catch { case ERROR(msg) => Output.warning(msg); no_markup }
wenzelm@58595
   168
            case None => no_markup
wenzelm@58546
   169
          }
wenzelm@58546
   170
wenzelm@58546
   171
        var offset = 0
wenzelm@58546
   172
        for ((style, token) <- styled_tokens) {
wenzelm@58546
   173
          val length = token.length
wenzelm@58546
   174
          val end_offset = offset + length
wenzelm@58546
   175
wenzelm@58546
   176
          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
wenzelm@58546
   177
            for (i <- offset until end_offset)
wenzelm@58546
   178
              handler.handleToken(line, style, i, 1, context1)
wenzelm@58546
   179
          }
wenzelm@58546
   180
          else handler.handleToken(line, style, offset, length, context1)
wenzelm@58546
   181
wenzelm@58546
   182
          offset += length
wenzelm@58546
   183
        }
wenzelm@58546
   184
        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
wenzelm@58546
   185
        context1
wenzelm@58546
   186
      }
wenzelm@58546
   187
      val context2 = context1.intern
wenzelm@58546
   188
      handler.setLineContext(context2)
wenzelm@58546
   189
      context2
wenzelm@58546
   190
    }
wenzelm@58546
   191
  }
wenzelm@58546
   192
wenzelm@58546
   193
wenzelm@58546
   194
wenzelm@58546
   195
  /** Sidekick parser **/
wenzelm@58546
   196
wenzelm@58546
   197
  class Sidekick_Parser extends SideKickParser("bibtex")
wenzelm@58546
   198
  {
wenzelm@58546
   199
    override def supportsCompletion = false
wenzelm@58546
   200
wenzelm@58747
   201
    private class Asset(label: String, label_html: String, range: Text.Range, source: String)
wenzelm@58747
   202
      extends Isabelle_Sidekick.Asset(label, range) {
wenzelm@58546
   203
        override def getShortString: String = label_html
wenzelm@58546
   204
        override def getLongString: String = source
wenzelm@58546
   205
      }
wenzelm@58546
   206
wenzelm@58546
   207
    def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
wenzelm@58546
   208
    {
wenzelm@58546
   209
      val data = Isabelle_Sidekick.root_data(buffer)
wenzelm@58546
   210
wenzelm@58546
   211
      try {
wenzelm@58546
   212
        var offset = 0
wenzelm@58546
   213
        for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
wenzelm@58546
   214
          val kind = chunk.kind
wenzelm@58546
   215
          val name = chunk.name
wenzelm@58546
   216
          val source = chunk.source
wenzelm@58546
   217
          if (kind != "") {
wenzelm@58546
   218
            val label = kind + (if (name == "") "" else " " + name)
wenzelm@58546
   219
            val label_html =
wenzelm@62113
   220
              "<html><b>" + HTML.output(kind) + "</b>" +
wenzelm@62113
   221
              (if (name == "") "" else " " + HTML.output(name)) + "</html>"
wenzelm@60215
   222
            val range = Text.Range(offset, offset + source.length)
wenzelm@58747
   223
            val asset = new Asset(label, label_html, range, source)
wenzelm@58546
   224
            data.root.add(new DefaultMutableTreeNode(asset))
wenzelm@58546
   225
          }
wenzelm@60215
   226
          offset += source.length
wenzelm@58546
   227
        }
wenzelm@58546
   228
        data
wenzelm@58546
   229
      }
wenzelm@58595
   230
      catch { case ERROR(msg) => Output.warning(msg); null }
wenzelm@58546
   231
    }
wenzelm@58546
   232
  }
wenzelm@58545
   233
}
wenzelm@58545
   234