author | wenzelm |
Mon, 02 Mar 2009 19:17:20 +0100 | |
changeset 34533 | 35308320713a |
parent 34507 | 018bad916757 |
child 34534 | b06946a1d4cb |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34408 | 2 |
* jEdit text area as document text source |
34407 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
5 |
* @author Johannes Hölzl, TU Munich |
|
34447 | 6 |
* @author Makarius |
34407 | 7 |
*/ |
8 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34446 | 11 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
import isabelle.proofdocument.Text |
34452 | 13 |
import isabelle.prover.{Prover, Command} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
import java.awt.Graphics2D |
34446 | 16 |
import java.awt.event.{ActionEvent, ActionListener} |
17 |
import java.awt.Color |
|
34447 | 18 |
import javax.swing.Timer |
19 |
import javax.swing.event.{CaretListener, CaretEvent} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
|
34446 | 21 |
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer} |
22 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
import org.gjt.sp.jedit.syntax.SyntaxStyle |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
24 |
|
34446 | 25 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
26 |
object TheoryView { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
|
34446 | 28 |
def choose_color(state: Command): Color = { |
34448 | 29 |
if (state == null) Color.red |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
30 |
else |
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
31 |
state.status match { |
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
32 |
case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
33 |
case Command.Status.FINISHED => new Color(234, 248, 255) |
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
34 |
case Command.Status.FAILED => new Color(255, 192, 192) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
case _ => Color.red |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
36 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
37 |
} |
34391 | 38 |
|
34446 | 39 |
def choose_color(markup: String): Color = { |
40 |
// TODO: as properties |
|
41 |
markup match { |
|
34445
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
42 |
// logical entities |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
43 |
case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
44 |
| Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
45 |
| Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255) |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
46 |
// inner syntax |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
47 |
case Markup.TFREE | Markup.FREE => Color.blue |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
48 |
case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
49 |
case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
50 |
| Markup.INNER_COMMENT => new Color(255, 128, 128) |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
51 |
case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP |
34446 | 52 |
| Markup.ATTRIBUTE | Markup.METHOD => Color.yellow |
34445
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
53 |
// embedded source text |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
54 |
case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
55 |
| Markup.DOC_ANTIQ => new Color(0, 192, 0) |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
56 |
// outer syntax |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
57 |
case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
58 |
case Markup.VERBATIM => Color.green |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
59 |
case Markup.COMMENT => Color.gray |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
60 |
case Markup.CONTROL => Color.white |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
61 |
case Markup.MALFORMED => Color.red |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
62 |
case Markup.STRING | Markup.ALTSTRING => Color.orange |
61ffe9a35f1d
use symbolic Markup elements instead of literal strings;
wenzelm
parents:
34440
diff
changeset
|
63 |
// other |
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
64 |
case _ => Color.white |
34391 | 65 |
} |
66 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
67 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
68 |
|
34446 | 69 |
|
70 |
class TheoryView (text_area: JEditTextArea) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
71 |
extends TextAreaExtension with Text with BufferListener { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
72 |
|
34446 | 73 |
private val buffer = text_area.getBuffer |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
74 |
private val prover = Isabelle.prover_setup(buffer).get.prover |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
75 |
buffer.addBufferListener(this) |
34446 | 76 |
|
77 |
||
78 |
private var col: Text.Changed = null |
|
79 |
||
80 |
private val col_timer = new Timer(300, new ActionListener() { |
|
81 |
override def actionPerformed(e: ActionEvent) = commit() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
82 |
}) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
83 |
|
34446 | 84 |
col_timer.stop |
85 |
col_timer.setRepeats(true) |
|
86 |
||
87 |
||
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
88 |
private val phase_overview = new PhaseOverviewPanel(prover) |
34446 | 89 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
90 |
|
34446 | 91 |
/* activation */ |
92 |
||
34456 | 93 |
Isabelle.plugin.font_changed += (_ => update_font()) |
34446 | 94 |
|
95 |
private def update_font() = { |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
96 |
if (text_area != null) { |
34440 | 97 |
if (Isabelle.plugin.font != null) { |
34446 | 98 |
val painter = text_area.getPainter |
34434 | 99 |
painter.setStyles(painter.getStyles.map(style => |
34446 | 100 |
new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
101 |
)) |
34440 | 102 |
painter.setFont(Isabelle.plugin.font) |
34446 | 103 |
repaint_all() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
104 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
105 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
106 |
} |
34446 | 107 |
|
108 |
private val selected_state_controller = new CaretListener { |
|
109 |
override def caretUpdate(e: CaretEvent) = { |
|
34496
1b2995592bb9
renamed getNextCommandContaining to find_command_at;
wenzelm
parents:
34475
diff
changeset
|
110 |
val cmd = prover.document.find_command_at(e.getDot) |
34446 | 111 |
if (cmd != null && cmd.start <= e.getDot && |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
112 |
Isabelle.prover_setup(buffer).get.selected_state != cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
113 |
Isabelle.prover_setup(buffer).get.selected_state = cmd |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
114 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
115 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
116 |
|
34446 | 117 |
def activate() = { |
118 |
text_area.addCaretListener(selected_state_controller) |
|
119 |
phase_overview.textarea = text_area |
|
120 |
text_area.addLeftOfScrollBar(phase_overview) |
|
121 |
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) |
|
122 |
update_font() |
|
123 |
} |
|
124 |
||
125 |
def deactivate() = { |
|
126 |
text_area.getPainter.removeExtension(this) |
|
127 |
text_area.removeLeftOfScrollBar(phase_overview) |
|
128 |
text_area.removeCaretListener(selected_state_controller) |
|
129 |
} |
|
130 |
||
131 |
||
132 |
/* painting */ |
|
133 |
||
134 |
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all()) |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
135 |
prover.command_info += (_ => repaint_delay.delay_or_ignore()) |
34446 | 136 |
|
137 |
private def from_current(pos: Int) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
138 |
if (col != null && col.start <= pos) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
139 |
if (pos < col.start + col.added) col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
140 |
else pos - col.added + col.removed |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
141 |
else pos |
34446 | 142 |
|
143 |
private def to_current(pos : Int) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
144 |
if (col != null && col.start <= pos) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
145 |
if (pos < col.start + col.removed) col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
else pos + col.added - col.removed |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
147 |
else pos |
34446 | 148 |
|
149 |
def repaint(cmd: Command) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
150 |
{ |
34507 | 151 |
if (text_area != null) { |
34446 | 152 |
val start = text_area.getLineOfOffset(to_current(cmd.start)) |
153 |
val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1) |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
154 |
text_area.invalidateLineRange(start, stop) |
34446 | 155 |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
156 |
if (Isabelle.prover_setup(buffer).get.selected_state == cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
157 |
Isabelle.prover_setup(buffer).get.selected_state = cmd // update State view |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
158 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
159 |
} |
34446 | 160 |
|
161 |
def repaint_all() = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
162 |
{ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
163 |
if (text_area != null) |
34446 | 164 |
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
165 |
} |
34391 | 166 |
|
34446 | 167 |
def encolor(gfx: Graphics2D, |
168 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) = |
|
169 |
{ |
|
170 |
val start = text_area.offsetToXY(begin) |
|
171 |
val stop = |
|
172 |
if (finish < buffer.getLength) text_area.offsetToXY(finish) |
|
173 |
else { |
|
174 |
val p = text_area.offsetToXY(finish - 1) |
|
175 |
p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ') |
|
176 |
p |
|
34391 | 177 |
} |
34446 | 178 |
|
179 |
if (start != null && stop != null) { |
|
180 |
gfx.setColor(color) |
|
181 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
|
182 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
|
183 |
} |
|
34391 | 184 |
} |
185 |
||
34446 | 186 |
|
187 |
/* TextAreaExtension methods */ |
|
188 |
||
189 |
override def paintValidLine(gfx: Graphics2D, |
|
34450 | 190 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) = |
34446 | 191 |
{ |
192 |
val saved_color = gfx.getColor |
|
193 |
||
194 |
val metrics = text_area.getPainter.getFontMetrics |
|
34496
1b2995592bb9
renamed getNextCommandContaining to find_command_at;
wenzelm
parents:
34475
diff
changeset
|
195 |
var e = prover.document.find_command_at(from_current(start)) |
34391 | 196 |
|
34446 | 197 |
// encolor phase |
198 |
while (e != null && to_current(e.start) < end) { |
|
199 |
val begin = start max to_current(e.start) |
|
200 |
val finish = end - 1 min to_current(e.stop) |
|
201 |
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true) |
|
202 |
||
34391 | 203 |
// paint details of command |
34446 | 204 |
for (node <- e.root_node.dfs) { |
205 |
val begin = to_current(node.start + e.start) |
|
206 |
val finish = to_current(node.end + e.start) |
|
207 |
if (finish > start && begin < end) { |
|
208 |
encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end, |
|
209 |
TheoryView.choose_color(node.short), true) |
|
210 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
211 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
212 |
e = e.next |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
213 |
} |
34391 | 214 |
|
34446 | 215 |
gfx.setColor(saved_color) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
216 |
} |
34446 | 217 |
|
218 |
||
219 |
/* Text methods */ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
220 |
|
34446 | 221 |
def content(start: Int, stop: Int) = buffer.getText(start, stop - start) |
222 |
def length = buffer.getLength |
|
34457 | 223 |
val changes = new EventBus[Text.Changed] |
34446 | 224 |
|
225 |
||
226 |
/* BufferListener methods */ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
227 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
228 |
private def commit() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
229 |
if (col != null) |
34456 | 230 |
changes.event(col) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
231 |
col = null |
34446 | 232 |
if (col_timer.isRunning()) |
233 |
col_timer.stop() |
|
234 |
} |
|
235 |
||
236 |
private def delay_commit() { |
|
237 |
if (col_timer.isRunning()) |
|
238 |
col_timer.restart() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
239 |
else |
34446 | 240 |
col_timer.start() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
241 |
} |
34446 | 242 |
|
243 |
||
244 |
override def contentInserted(buffer: JEditBuffer, |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
245 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
34446 | 246 |
{ |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
247 |
/* |
34364 | 248 |
if (col == null) |
34446 | 249 |
col = new Text.Changed(offset, length, 0) |
250 |
else if (col.start <= offset && offset <= col.start + col.added) |
|
251 |
col = new Text.Changed(col.start, col.added + length, col.removed) |
|
252 |
else { |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
253 |
commit() |
34446 | 254 |
col = new Text.Changed(offset, length, 0) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
255 |
} |
34446 | 256 |
delay_commit() |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
257 |
*/ |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
258 |
changes.event(new Text.Changed(offset, length, 0)) |
34446 | 259 |
} |
260 |
||
261 |
override def preContentRemoved(buffer: JEditBuffer, |
|
262 |
start_line: Int, start: Int, num_lines: Int, removed: Int) = |
|
263 |
{ |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
264 |
/* |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
265 |
if (col == null) |
34446 | 266 |
col = new Text.Changed(start, 0, removed) |
267 |
else if (col.start > start + removed || start > col.start + col.added) { |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
268 |
commit() |
34446 | 269 |
col = new Text.Changed(start, 0, removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
270 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
271 |
else { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
272 |
val offset = start - col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
273 |
val diff = col.added - removed |
34446 | 274 |
val (added, add_removed) = |
275 |
if (diff < offset) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
276 |
(offset max 0, diff - (offset max 0)) |
34446 | 277 |
else |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
278 |
(diff - (offset min 0), offset min 0) |
34446 | 279 |
col = new Text.Changed(start min col.start, added, col.removed - add_removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
280 |
} |
34446 | 281 |
delay_commit() |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
282 |
*/ |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
283 |
changes.event(new Text.Changed(start, 0, removed)) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
284 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
285 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
286 |
override def contentRemoved(buffer: JEditBuffer, |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
287 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
288 |
override def preContentInserted(buffer: JEditBuffer, |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34507
diff
changeset
|
289 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
34446 | 290 |
override def bufferLoaded(buffer: JEditBuffer) { } |
291 |
override def foldHandlerChanged(buffer: JEditBuffer) { } |
|
292 |
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } |
|
293 |
override def transactionComplete(buffer: JEditBuffer) { } |
|
34447 | 294 |
} |