58529
|
1 |
/* Title: Tools/jEdit/src/bibtex_token_markup.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Bibtex token markup.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
|
|
13 |
|
|
14 |
import javax.swing.text.Segment
|
|
15 |
|
|
16 |
|
|
17 |
object Bibtex_Token_Markup
|
|
18 |
{
|
|
19 |
/* token style */
|
|
20 |
|
58530
|
21 |
private def token_style(context: String, token: Bibtex.Token): Byte =
|
58529
|
22 |
token.kind match {
|
|
23 |
case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
|
|
24 |
case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
|
|
25 |
case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
|
|
26 |
case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
|
|
27 |
case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
|
58531
|
28 |
case Bibtex.Token.Kind.NAME => JEditToken.LABEL
|
58529
|
29 |
case Bibtex.Token.Kind.IDENT =>
|
|
30 |
if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
|
|
31 |
else
|
58530
|
32 |
Bibtex.get_entry(context) match {
|
58529
|
33 |
case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
|
|
34 |
case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
|
|
35 |
case _ => JEditToken.DIGIT
|
|
36 |
}
|
|
37 |
case Bibtex.Token.Kind.IGNORED => JEditToken.NULL
|
|
38 |
case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
|
|
39 |
}
|
|
40 |
|
|
41 |
|
|
42 |
/* line context */
|
|
43 |
|
|
44 |
private val context_rules = new ParserRuleSet("bibtex", "MAIN")
|
|
45 |
|
|
46 |
private class Line_Context(context: Option[Bibtex.Line_Context])
|
|
47 |
extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
|
|
48 |
|
|
49 |
|
|
50 |
/* token marker */
|
|
51 |
|
|
52 |
class Marker extends TokenMarker
|
|
53 |
{
|
|
54 |
override def markTokens(context: TokenMarker.LineContext,
|
|
55 |
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
|
|
56 |
{
|
|
57 |
val line_ctxt =
|
|
58 |
context match {
|
|
59 |
case c: Line_Context => c.context
|
|
60 |
case _ => Some(Bibtex.Ignored_Context)
|
|
61 |
}
|
|
62 |
val line = if (raw_line == null) new Segment else raw_line
|
|
63 |
|
|
64 |
val context1 =
|
|
65 |
{
|
|
66 |
val (styled_tokens, context1) =
|
|
67 |
line_ctxt match {
|
|
68 |
case Some(ctxt) =>
|
|
69 |
val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
|
|
70 |
val styled_tokens =
|
|
71 |
for { chunk <- chunks; tok <- chunk.tokens }
|
|
72 |
yield (token_style(chunk.kind, tok), tok.source)
|
|
73 |
(styled_tokens, new Line_Context(Some(ctxt1)))
|
|
74 |
case None =>
|
|
75 |
val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
|
|
76 |
(List(styled_token), new Line_Context(None))
|
|
77 |
}
|
|
78 |
|
|
79 |
var offset = 0
|
|
80 |
for ((style, token) <- styled_tokens) {
|
|
81 |
val length = token.length
|
|
82 |
val end_offset = offset + length
|
|
83 |
handler.handleToken(line, style, offset, length, context1)
|
|
84 |
offset += length
|
|
85 |
}
|
|
86 |
handler.handleToken(line, JEditToken.END, line.count, 0, context1)
|
|
87 |
context1
|
|
88 |
}
|
|
89 |
val context2 = context1.intern
|
|
90 |
handler.setLineContext(context2)
|
|
91 |
context2
|
|
92 |
}
|
|
93 |
}
|
|
94 |
}
|
|
95 |
|