author | immler@in.tum.de |
Wed, 27 May 2009 17:13:58 +0200 | |
changeset 34579 | f5c3ad245539 |
parent 34564 | 850dc36d4926 |
child 34582 | 5d5d253c7c29 |
child 34596 | 2b46d92e4642 |
permissions | -rw-r--r-- |
34467 | 1 |
/* |
2 |
* include isabelle's command- and keyword-declarations |
|
3 |
* live in jEdits syntax-highlighting |
|
34517 | 4 |
* |
34467 | 5 |
* @author Fabian Immler, TU Munich |
6 |
*/ |
|
7 |
||
8 |
package isabelle.jedit |
|
9 |
||
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34524
diff
changeset
|
10 |
import isabelle.prover.{Command, MarkupNode, Prover} |
34517 | 11 |
import isabelle.Markup |
34467 | 12 |
|
34517 | 13 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
14 |
import org.gjt.sp.jedit.syntax._ |
|
34467 | 15 |
|
34517 | 16 |
import java.awt.Color |
17 |
import java.awt.Font |
|
18 |
import javax.swing.text.Segment; |
|
19 |
||
20 |
object DynamicTokenMarker { |
|
34467 | 21 |
|
34549 | 22 |
// Mapping to jEdits token types |
23 |
def choose_byte(kind: String): Byte = { |
|
24 |
// TODO: as properties |
|
25 |
kind match { |
|
26 |
// logical entities |
|
27 |
case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL |
|
28 |
| Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT |
|
29 |
| Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => Token.DIGIT |
|
30 |
// inner syntax |
|
31 |
case Markup.TFREE | Markup.FREE => Token.LITERAL2 |
|
32 |
case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Token.LITERAL3 |
|
33 |
case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL |
|
34 |
| Markup.INNER_COMMENT => Token.LITERAL4 |
|
35 |
case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP |
|
36 |
| Markup.ATTRIBUTE | Markup.METHOD => Token.FUNCTION |
|
37 |
// ML syntax |
|
38 |
case Markup.ML_KEYWORD => Token.KEYWORD2 |
|
39 |
case Markup.ML_IDENT => Token.KEYWORD3 |
|
40 |
case Markup.ML_TVAR => Token.LITERAL3 |
|
41 |
case Markup.ML_NUMERAL => Token.LITERAL4 |
|
42 |
case Markup.ML_CHAR | Markup.ML_STRING => Token.LITERAL1 |
|
43 |
case Markup.ML_COMMENT => Token.COMMENT1 |
|
44 |
case Markup.ML_MALFORMED => Token.INVALID |
|
45 |
// embedded source text |
|
46 |
case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ |
|
47 |
| Markup.DOC_ANTIQ => Token.COMMENT4 |
|
48 |
// outer syntax |
|
49 |
case Markup.IDENT => Token.KEYWORD3 |
|
50 |
case Markup.COMMAND => Token.KEYWORD1 |
|
51 |
case Markup.KEYWORD => Token.KEYWORD2 |
|
52 |
case Markup.VERBATIM => Token.COMMENT1 |
|
53 |
case Markup.COMMENT => Token.COMMENT2 |
|
54 |
case Markup.CONTROL => Token.COMMENT3 |
|
55 |
case Markup.MALFORMED => Token.INVALID |
|
56 |
case Markup.STRING | Markup.ALTSTRING => Token.LITERAL1 |
|
57 |
// other |
|
58 |
case _ => 0 |
|
59 |
} |
|
34517 | 60 |
} |
34467 | 61 |
|
34579
f5c3ad245539
outer syntax could clash with status on removed commands
immler@in.tum.de
parents:
34564
diff
changeset
|
62 |
def is_outer(kind: String) = |
f5c3ad245539
outer syntax could clash with status on removed commands
immler@in.tum.de
parents:
34564
diff
changeset
|
63 |
List(Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT, |
f5c3ad245539
outer syntax could clash with status on removed commands
immler@in.tum.de
parents:
34564
diff
changeset
|
64 |
Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING).exists(kind == _) |
f5c3ad245539
outer syntax could clash with status on removed commands
immler@in.tum.de
parents:
34564
diff
changeset
|
65 |
|
34549 | 66 |
def choose_color(kind : String, styles: Array[SyntaxStyle]) : Color = |
67 |
styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor |
|
34517 | 68 |
|
34467 | 69 |
} |
34517 | 70 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34524
diff
changeset
|
71 |
class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker { |
34517 | 72 |
|
73 |
override def markTokens(prev: TokenMarker.LineContext, |
|
74 |
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { |
|
75 |
val previous = prev.asInstanceOf[IndexLineContext] |
|
76 |
val line = if(prev == null) 0 else previous.line + 1 |
|
77 |
val context = new IndexLineContext(line, previous) |
|
78 |
val start = buffer.getLineStartOffset(line) |
|
79 |
val stop = start + line_segment.count |
|
34541 | 80 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
81 |
val document = prover.document |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
82 |
|
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
83 |
def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(document.id, _) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
84 |
def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _) |
34517 | 85 |
|
34522 | 86 |
var next_x = start |
87 |
for { |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
88 |
command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop)) |
34556 | 89 |
markup <- command.highlight_node.flatten |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
90 |
if(to(markup.abs_stop(document)) > start) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
91 |
if(to(markup.abs_start(document)) < stop) |
34564
850dc36d4926
let MarkupNode carry arbitrary information
immler@in.tum.de
parents:
34556
diff
changeset
|
92 |
byte = DynamicTokenMarker.choose_byte(markup.info.toString) |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
93 |
token_start = to(markup.abs_start(document)) - start max 0 |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
94 |
token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) - |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
95 |
(start - to(markup.abs_start(document)) max 0) - |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
96 |
(to(markup.abs_stop(document)) - stop max 0) |
34522 | 97 |
} { |
98 |
if (start + token_start > next_x) |
|
99 |
handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context) |
|
100 |
handler.handleToken(line_segment, byte, token_start, token_length, context) |
|
101 |
next_x = start + token_start + token_length |
|
34517 | 102 |
} |
34522 | 103 |
if (next_x < stop) |
104 |
handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context) |
|
34517 | 105 |
|
106 |
handler.handleToken(line_segment,Token.END, line_segment.count, 0, context) |
|
107 |
handler.setLineContext(context) |
|
108 |
return context |
|
109 |
} |
|
110 |
||
111 |
} |
|
112 |
||
113 |
class IndexLineContext(val line: Int, prev: IndexLineContext) |
|
114 |
extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev) |