43414
|
1 |
/* Title: Tools/jEdit/src/token_markup.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Outer syntax token markup.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import org.gjt.sp.jedit.Buffer
|
|
13 |
import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
|
|
14 |
import javax.swing.text.Segment
|
|
15 |
|
|
16 |
|
|
17 |
object Token_Markup
|
|
18 |
{
|
|
19 |
/* extended jEdit syntax styles */
|
|
20 |
|
|
21 |
private val plain_range: Int = JToken.ID_COUNT
|
|
22 |
private def check_range(i: Int) { require(0 <= i && i < plain_range) }
|
|
23 |
|
|
24 |
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
|
|
25 |
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
|
|
26 |
val hidden: Byte = (3 * plain_range).toByte
|
|
27 |
|
|
28 |
|
|
29 |
/* token marker */
|
|
30 |
|
|
31 |
private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
|
|
32 |
|
|
33 |
private class Line_Context(val context: Scan.Context)
|
|
34 |
extends TokenMarker.LineContext(isabelle_rules, null)
|
|
35 |
{
|
|
36 |
override def hashCode: Int = context.hashCode
|
|
37 |
override def equals(that: Any): Boolean =
|
|
38 |
that match {
|
|
39 |
case other: Line_Context => context == other.context
|
|
40 |
case _ => false
|
|
41 |
}
|
|
42 |
}
|
|
43 |
|
|
44 |
def token_marker(session: Session, buffer: Buffer): TokenMarker =
|
|
45 |
new TokenMarker {
|
|
46 |
override def markTokens(context: TokenMarker.LineContext,
|
|
47 |
handler: TokenHandler, line: Segment): TokenMarker.LineContext =
|
|
48 |
{
|
|
49 |
Isabelle.swing_buffer_lock(buffer) {
|
|
50 |
val syntax = session.current_syntax()
|
|
51 |
|
|
52 |
val ctxt =
|
|
53 |
context match {
|
|
54 |
case c: Line_Context => c.context
|
|
55 |
case _ => Scan.Finished
|
|
56 |
}
|
|
57 |
|
|
58 |
val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
|
|
59 |
val context1 = new Line_Context(ctxt1)
|
|
60 |
|
|
61 |
var offset = 0
|
|
62 |
for (token <- tokens) {
|
|
63 |
val style = Isabelle_Markup.token_markup(syntax, token)
|
|
64 |
val length = token.source.length
|
|
65 |
handler.handleToken(line, style, offset, length, context1)
|
|
66 |
offset += length
|
|
67 |
}
|
|
68 |
handler.handleToken(line, JToken.END, line.count, 0, context1)
|
|
69 |
handler.setLineContext(context1)
|
|
70 |
context1
|
|
71 |
}
|
|
72 |
}
|
|
73 |
}
|
|
74 |
}
|
|
75 |
|