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 |
|
21 private def token_style(context: String, token: Bibtex.Token): Byte = |
|
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 |
|
28 case Bibtex.Token.Kind.NAME => JEditToken.LABEL |
|
29 case Bibtex.Token.Kind.IDENT => |
|
30 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 |
|
31 else |
|
32 Bibtex.get_entry(context) match { |
|
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.SPACE => JEditToken.NULL |
|
38 case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1 |
|
39 case Bibtex.Token.Kind.ERROR => JEditToken.INVALID |
|
40 } |
|
41 |
|
42 |
|
43 /* line context */ |
|
44 |
|
45 private val context_rules = new ParserRuleSet("bibtex", "MAIN") |
|
46 |
|
47 private class Line_Context(context: Option[Bibtex.Line_Context]) |
|
48 extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context) |
|
49 |
|
50 |
|
51 /* token marker */ |
|
52 |
|
53 class Marker extends TokenMarker |
|
54 { |
|
55 override def markTokens(context: TokenMarker.LineContext, |
|
56 handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = |
|
57 { |
|
58 val line_ctxt = |
|
59 context match { |
|
60 case c: Line_Context => c.context |
|
61 case _ => Some(Bibtex.Ignored_Context) |
|
62 } |
|
63 val line = if (raw_line == null) new Segment else raw_line |
|
64 |
|
65 val context1 = |
|
66 { |
|
67 val (styled_tokens, context1) = |
|
68 line_ctxt match { |
|
69 case Some(ctxt) => |
|
70 val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt) |
|
71 val styled_tokens = |
|
72 for { chunk <- chunks; tok <- chunk.tokens } |
|
73 yield (token_style(chunk.kind, tok), tok.source) |
|
74 (styled_tokens, new Line_Context(Some(ctxt1))) |
|
75 case None => |
|
76 val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) |
|
77 (List(styled_token), new Line_Context(None)) |
|
78 } |
|
79 |
|
80 var offset = 0 |
|
81 for ((style, token) <- styled_tokens) { |
|
82 val length = token.length |
|
83 val end_offset = offset + length |
|
84 |
|
85 if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) { |
|
86 for (i <- offset until end_offset) |
|
87 handler.handleToken(line, style, i, 1, context1) |
|
88 } |
|
89 else handler.handleToken(line, style, offset, length, context1) |
|
90 |
|
91 offset += length |
|
92 } |
|
93 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
|
94 context1 |
|
95 } |
|
96 val context2 = context1.intern |
|
97 handler.setLineContext(context2) |
|
98 context2 |
|
99 } |
|
100 } |
|
101 } |
|
102 |
|