src/Tools/jEdit/src/bibtex_jedit.scala
author wenzelm
Tue, 20 Dec 2016 21:35:56 +0100
changeset 64621 7116f2634e32
parent 62113 16de2a9b5b3d
child 64813 7283f41d05ab
permissions -rw-r--r--
clarified module name;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/bibtex_jedit.scala
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     3
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     4
BibTeX support in Isabelle/jEdit.
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     5
*/
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     6
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     8
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
     9
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    10
import isabelle._
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    11
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    12
58547
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    13
import scala.collection.mutable
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    14
58548
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
    15
import java.awt.event.{ActionListener, ActionEvent}
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
    16
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    17
import javax.swing.text.Segment
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    18
import javax.swing.tree.DefaultMutableTreeNode
58548
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
    19
import javax.swing.{JMenu, JMenuItem}
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    20
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    21
import org.gjt.sp.jedit.Buffer
58548
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    23
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    24
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    25
import sidekick.{SideKickParser, SideKickParsedData}
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    26
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    27
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    28
object Bibtex_JEdit
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    29
{
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    30
  /** buffer model **/
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    31
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    32
  /* file type */
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    33
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    34
  def check(buffer: Buffer): Boolean =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    35
    JEdit_Lib.buffer_name(buffer).endsWith(".bib")
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    36
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    37
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    38
  /* parse entries */
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    39
58547
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    40
  def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] =
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    41
  {
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    42
    val chunks =
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    43
      try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) }
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    44
      catch { case ERROR(msg) => Output.warning(msg); Nil }
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    45
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    46
    val result = new mutable.ListBuffer[(String, Text.Offset)]
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    47
    var offset = 0
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    48
    for (chunk <- chunks) {
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    49
      if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset))
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    50
      offset += chunk.source.length
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    51
    }
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    52
    result.toList
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    53
  }
6080615b8b96 clarified modules;
wenzelm
parents: 58546
diff changeset
    54
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    55
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    56
  /* retrieve entries */
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    57
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    58
  def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    59
    for {
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    60
      buffer <- JEdit_Lib.jedit_buffers()
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    61
      model <- PIDE.document_model(buffer).iterator
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    62
      (name, offset) <- model.bibtex_entries.iterator
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
    63
    } yield (name, buffer, offset)
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    64
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
    65
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    66
  /* completion */
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    67
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    68
  def complete(name: String): List[String] =
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    69
  {
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    70
    val name1 = name.toLowerCase
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    71
    (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1))
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    72
      yield entry).toList
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    73
  }
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    74
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    75
  def completion(
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    76
    history: Completion.History,
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    77
    text_area: JEditTextArea,
64621
7116f2634e32 clarified module name;
wenzelm
parents: 62113
diff changeset
    78
    rendering: JEdit_Rendering): Option[Completion.Result] =
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    79
  {
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    80
    for {
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    81
      Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
61100
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    82
      name1 <- Completion.clean_name(name)
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    83
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    84
      original <- JEdit_Lib.try_get_text(text_area.getBuffer, r)
61100
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    85
      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    86
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    87
      entries = complete(name1).filter(_ != original1)
59319
wenzelm
parents: 59062
diff changeset
    88
      if entries.nonEmpty
61100
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 61099
diff changeset
    89
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    90
      items =
61099
64dcd8609962 use alphabetic order before history order;
wenzelm
parents: 60215
diff changeset
    91
        entries.sorted.map({
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    92
          case entry =>
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    93
            val full_name = Long_Name.qualify(Markup.CITATION, entry)
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    94
            val description = List(entry, "(BibTeX entry)")
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    95
            val replacement = quote(entry)
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    96
          Completion.Item(r, original, full_name, description, replacement, 0, false)
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    97
        }).sorted(history.ordering).take(PIDE.options.int("completion_limit"))
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    98
    } yield Completion.Result(r, original, false, items)
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
    99
  }
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
   100
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 58589
diff changeset
   101
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   102
58548
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   103
  /** context menu **/
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   104
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   105
  def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   106
  {
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   107
    text_area0 match {
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   108
      case text_area: TextArea =>
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   109
        text_area.getBuffer match {
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   110
          case buffer: Buffer
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   111
          if (check(buffer) && buffer.isEditable) =>
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   112
            val menu = new JMenu("BibTeX entries")
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   113
            for (entry <- Bibtex.entries) {
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   114
              val item = new JMenuItem(entry.kind)
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   115
              item.addActionListener(new ActionListener {
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   116
                def actionPerformed(evt: ActionEvent): Unit =
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   117
                  Isabelle.insert_line_padding(text_area, entry.template)
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   118
              })
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   119
              menu.add(item)
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   120
            }
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   121
            List(menu)
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   122
          case _ => Nil
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   123
        }
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   124
      case _ => Nil
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   125
    }
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   126
  }
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   127
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   128
d0ee64efd624 clarified modules;
wenzelm
parents: 58547
diff changeset
   129
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   130
  /** token markup **/
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   131
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   132
  /* token style */
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   133
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   134
  private def token_style(context: String, token: Bibtex.Token): Byte =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   135
    token.kind match {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   136
      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   137
      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   138
      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   139
      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   140
      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   141
      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   142
      case Bibtex.Token.Kind.IDENT =>
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   143
        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   144
        else
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   145
          Bibtex.get_entry(context) match {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   146
            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   147
            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   148
            case _ => JEditToken.DIGIT
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   149
          }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   150
      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   151
      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   152
      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   153
    }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   154
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   155
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   156
  /* line context */
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   157
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   158
  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   159
58699
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   160
  private class Line_Context(val context: Option[Bibtex.Line_Context])
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   161
    extends TokenMarker.LineContext(context_rules, null)
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   162
  {
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   163
    override def hashCode: Int = context.hashCode
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   164
    override def equals(that: Any): Boolean =
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   165
      that match {
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   166
        case other: Line_Context => context == other.context
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   167
        case _ => false
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   168
      }
e46afcceb781 tuned signature;
wenzelm
parents: 58698
diff changeset
   169
  }
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   170
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   171
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   172
  /* token marker */
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   173
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   174
  class Token_Marker extends TokenMarker
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   175
  {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   176
    override def markTokens(context: TokenMarker.LineContext,
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   177
        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   178
    {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   179
      val line_ctxt =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   180
        context match {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   181
          case c: Line_Context => c.context
58589
d9350ec0937e tuned signature;
wenzelm
parents: 58548
diff changeset
   182
          case _ => Some(Bibtex.Ignored)
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   183
        }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   184
      val line = if (raw_line == null) new Segment else raw_line
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   185
58595
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   186
      def no_markup =
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   187
      {
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   188
        val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   189
        (List(styled_token), new Line_Context(None))
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   190
      }
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   191
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   192
      val context1 =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   193
      {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   194
        val (styled_tokens, context1) =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   195
          line_ctxt match {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   196
            case Some(ctxt) =>
58595
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   197
              try {
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   198
                val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   199
                val styled_tokens =
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   200
                  for { chunk <- chunks; tok <- chunk.tokens }
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   201
                  yield (token_style(chunk.kind, tok), tok.source)
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   202
                (styled_tokens, new Line_Context(Some(ctxt1)))
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   203
              }
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   204
              catch { case ERROR(msg) => Output.warning(msg); no_markup }
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   205
            case None => no_markup
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   206
          }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   207
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   208
        var offset = 0
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   209
        for ((style, token) <- styled_tokens) {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   210
          val length = token.length
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   211
          val end_offset = offset + length
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   212
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   213
          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   214
            for (i <- offset until end_offset)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   215
              handler.handleToken(line, style, i, 1, context1)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   216
          }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   217
          else handler.handleToken(line, style, offset, length, context1)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   218
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   219
          offset += length
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   220
        }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   221
        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   222
        context1
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   223
      }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   224
      val context2 = context1.intern
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   225
      handler.setLineContext(context2)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   226
      context2
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   227
    }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   228
  }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   229
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   230
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   231
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   232
  /** Sidekick parser **/
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   233
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   234
  class Sidekick_Parser extends SideKickParser("bibtex")
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   235
  {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   236
    override def supportsCompletion = false
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   237
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58699
diff changeset
   238
    private class Asset(label: String, label_html: String, range: Text.Range, source: String)
c680f181b32e tuned rendering;
wenzelm
parents: 58699
diff changeset
   239
      extends Isabelle_Sidekick.Asset(label, range) {
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   240
        override def getShortString: String = label_html
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   241
        override def getLongString: String = source
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   242
      }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   243
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   244
    def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   245
    {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   246
      val data = Isabelle_Sidekick.root_data(buffer)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   247
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   248
      try {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   249
        var offset = 0
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   250
        for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   251
          val kind = chunk.kind
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   252
          val name = chunk.name
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   253
          val source = chunk.source
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   254
          if (kind != "") {
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   255
            val label = kind + (if (name == "") "" else " " + name)
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   256
            val label_html =
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 61100
diff changeset
   257
              "<html><b>" + HTML.output(kind) + "</b>" +
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 61100
diff changeset
   258
              (if (name == "") "" else " " + HTML.output(name)) + "</html>"
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   259
            val range = Text.Range(offset, offset + source.length)
58747
c680f181b32e tuned rendering;
wenzelm
parents: 58699
diff changeset
   260
            val asset = new Asset(label, label_html, range, source)
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   261
            data.root.add(new DefaultMutableTreeNode(asset))
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   262
          }
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   263
          offset += source.length
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   264
        }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   265
        data
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   266
      }
58595
127f192b755c more defensive error handling -- token marker must not crash;
wenzelm
parents: 58592
diff changeset
   267
      catch { case ERROR(msg) => Output.warning(msg); null }
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   268
    }
72e2b2a609c4 clarified modules;
wenzelm
parents: 58545
diff changeset
   269
  }
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
   270
}
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff changeset
   271