1/*  Title:      Tools/jEdit/src/jedit_bibtex.scala
2    Author:     Makarius
3
4BibTeX support in Isabelle/jEdit.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11
12
13import scala.collection.mutable
14
15import java.awt.event.{ActionListener, ActionEvent}
16
17import javax.swing.text.Segment
18import javax.swing.tree.DefaultMutableTreeNode
19import javax.swing.{JMenu, JMenuItem}
20
21import org.gjt.sp.jedit.Buffer
22import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
23import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
24
25import sidekick.{SideKickParser, SideKickParsedData}
26
27
28object JEdit_Bibtex
29{
30  /** context menu **/
31
32  def context_menu(text_area0: JEditTextArea): List[JMenuItem] =
33  {
34    text_area0 match {
35      case text_area: TextArea =>
36        text_area.getBuffer match {
37          case buffer: Buffer
38          if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
39            val menu = new JMenu("BibTeX entries")
40            for (entry <- Bibtex.known_entries) {
41              val item = new JMenuItem(entry.kind)
42              item.addActionListener(new ActionListener {
43                def actionPerformed(evt: ActionEvent): Unit =
44                  Isabelle.insert_line_padding(text_area, entry.template)
45              })
46              menu.add(item)
47            }
48            List(menu)
49          case _ => Nil
50        }
51      case _ => Nil
52    }
53  }
54
55
56
57  /** token markup **/
58
59  /* token style */
60
61  private def token_style(context: String, token: Bibtex.Token): Byte =
62    token.kind match {
63      case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
64      case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
65      case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
66      case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
67      case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
68      case Bibtex.Token.Kind.NAME => JEditToken.LABEL
69      case Bibtex.Token.Kind.IDENT =>
70        if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
71        else
72          Bibtex.get_entry(context) match {
73            case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
74            case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
75            case _ => JEditToken.DIGIT
76          }
77      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
78      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
79      case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
80    }
81
82
83  /* line context */
84
85  private val context_rules = new ParserRuleSet("bibtex", "MAIN")
86
87  private class Line_Context(val context: Option[Bibtex.Line_Context])
88    extends TokenMarker.LineContext(context_rules, null)
89  {
90    override def hashCode: Int = context.hashCode
91    override def equals(that: Any): Boolean =
92      that match {
93        case other: Line_Context => context == other.context
94        case _ => false
95      }
96  }
97
98
99  /* token marker */
100
101  class Token_Marker extends TokenMarker
102  {
103    override def markTokens(context: TokenMarker.LineContext,
104        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
105    {
106      val line_ctxt =
107        context match {
108          case c: Line_Context => c.context
109          case _ => Some(Bibtex.Ignored)
110        }
111      val line = if (raw_line == null) new Segment else raw_line
112
113      def no_markup =
114      {
115        val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
116        (List(styled_token), new Line_Context(None))
117      }
118
119      val context1 =
120      {
121        val (styled_tokens, context1) =
122          line_ctxt match {
123            case Some(ctxt) =>
124              try {
125                val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
126                val styled_tokens =
127                  for { chunk <- chunks; tok <- chunk.tokens }
128                  yield (token_style(chunk.kind, tok), tok.source)
129                (styled_tokens, new Line_Context(Some(ctxt1)))
130              }
131              catch { case ERROR(msg) => Output.warning(msg); no_markup }
132            case None => no_markup
133          }
134
135        var offset = 0
136        for ((style, token) <- styled_tokens) {
137          val length = token.length
138          val end_offset = offset + length
139
140          if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
141            for (i <- offset until end_offset)
142              handler.handleToken(line, style, i, 1, context1)
143          }
144          else handler.handleToken(line, style, offset, length, context1)
145
146          offset += length
147        }
148        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
149        context1
150      }
151      val context2 = context1.intern
152      handler.setLineContext(context2)
153      context2
154    }
155  }
156
157
158
159  /** Sidekick parser **/
160
161  class Sidekick_Parser extends SideKickParser("bibtex")
162  {
163    override def supportsCompletion = false
164
165    private class Asset(label: String, label_html: String, range: Text.Range, source: String)
166      extends Isabelle_Sidekick.Asset(label, range) {
167        override def getShortString: String = label_html
168        override def getLongString: String = source
169      }
170
171    def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
172    {
173      val data = Isabelle_Sidekick.root_data(buffer)
174
175      try {
176        var offset = 0
177        for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
178          val kind = chunk.kind
179          val name = chunk.name
180          val source = chunk.source
181          if (kind != "") {
182            val label = kind + (if (name == "") "" else " " + name)
183            val label_html =
184              "<html><b>" + HTML.output(kind) + "</b>" +
185              (if (name == "") "" else " " + HTML.output(name)) + "</html>"
186            val range = Text.Range(offset, offset + source.length)
187            val asset = new Asset(label, label_html, range, source)
188            data.root.add(new DefaultMutableTreeNode(asset))
189          }
190          offset += source.length
191        }
192        data
193      }
194      catch { case ERROR(msg) => Output.warning(msg); null }
195    }
196  }
197}
198