author | immler@in.tum.de |
Tue, 07 Apr 2009 21:30:47 +0200 | |
changeset 34546 | 3ed38cf4164a |
parent 34545 | b928628742ed |
child 34547 | 68a5e91ac3a3 |
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 |
|
34532 | 11 |
import scala.actors.Actor |
34446 | 12 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
import isabelle.proofdocument.Text |
34452 | 14 |
import isabelle.prover.{Prover, Command} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
import java.awt.Graphics2D |
34446 | 17 |
import java.awt.event.{ActionEvent, ActionListener} |
18 |
import java.awt.Color |
|
34447 | 19 |
import javax.swing.Timer |
20 |
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
|
21 |
|
34446 | 22 |
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer} |
23 |
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
|
24 |
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
|
25 |
|
34446 | 26 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
object TheoryView { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
28 |
|
34446 | 29 |
def choose_color(state: Command): Color = { |
34448 | 30 |
if (state == null) Color.red |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
31 |
else |
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
32 |
state.status match { |
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34457
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
case _ => Color.red |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
37 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
38 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
39 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
40 |
|
34446 | 41 |
|
34532 | 42 |
class TheoryView (text_area: JEditTextArea, document_actor: Actor) |
43 |
extends TextAreaExtension with BufferListener { |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
44 |
|
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset
|
45 |
def id() = Isabelle.plugin.id(); |
34541 | 46 |
|
34446 | 47 |
private val buffer = text_area.getBuffer |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
48 |
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
|
49 |
buffer.addBufferListener(this) |
34446 | 50 |
|
51 |
||
34526 | 52 |
private var col: Text.Change = null |
34446 | 53 |
|
54 |
private val col_timer = new Timer(300, new ActionListener() { |
|
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
55 |
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
|
56 |
}) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
57 |
|
34446 | 58 |
col_timer.stop |
59 |
col_timer.setRepeats(true) |
|
60 |
||
61 |
||
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
62 |
private val phase_overview = new PhaseOverviewPanel(prover, to_current) |
34446 | 63 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
64 |
|
34446 | 65 |
/* activation */ |
66 |
||
34517 | 67 |
Isabelle.plugin.font_changed += (_ => update_styles) |
34446 | 68 |
|
34517 | 69 |
private def update_styles = { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
70 |
if (text_area != null) { |
34440 | 71 |
if (Isabelle.plugin.font != null) { |
34524 | 72 |
text_area.getPainter.setStyles(DynamicTokenMarker.reload_styles) |
34517 | 73 |
repaint_all |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
74 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
75 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
76 |
} |
34446 | 77 |
|
78 |
private val selected_state_controller = new CaretListener { |
|
79 |
override def caretUpdate(e: CaretEvent) = { |
|
34496
1b2995592bb9
renamed getNextCommandContaining to find_command_at;
wenzelm
parents:
34475
diff
changeset
|
80 |
val cmd = prover.document.find_command_at(e.getDot) |
34446 | 81 |
if (cmd != null && cmd.start <= e.getDot && |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
82 |
Isabelle.prover_setup(buffer).get.selected_state != cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
83 |
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
|
84 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
85 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
86 |
|
34446 | 87 |
def activate() = { |
88 |
text_area.addCaretListener(selected_state_controller) |
|
89 |
phase_overview.textarea = text_area |
|
90 |
text_area.addLeftOfScrollBar(phase_overview) |
|
91 |
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
92 |
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) |
34517 | 93 |
update_styles |
34541 | 94 |
document_actor ! new Text.Change(id(), 0,buffer.getText(0, buffer.getLength),0) |
34446 | 95 |
} |
96 |
||
97 |
def deactivate() = { |
|
98 |
text_area.getPainter.removeExtension(this) |
|
99 |
text_area.removeLeftOfScrollBar(phase_overview) |
|
100 |
text_area.removeCaretListener(selected_state_controller) |
|
101 |
} |
|
102 |
||
103 |
||
104 |
/* painting */ |
|
105 |
||
106 |
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all()) |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
107 |
|
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
108 |
val change_receiver = scala.actors.Actor.actor { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
109 |
scala.actors.Actor.loop { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
110 |
scala.actors.Actor.react { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
111 |
case _ => { |
34541 | 112 |
Swing.now { |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
113 |
repaint_delay.delay_or_ignore() |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
114 |
phase_overview.repaint_delay.delay_or_ignore() |
34541 | 115 |
} |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
116 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
117 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
118 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
119 |
}.start |
34446 | 120 |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
121 |
def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int = |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
122 |
changes match { |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
123 |
case Nil => pos |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
124 |
case Text.Change(id, start, added, removed) :: rest_changes => { |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
125 |
val shifted = if (start <= pos) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
126 |
if (pos < start + added.length) start |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
127 |
else pos - added.length + removed |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
128 |
else pos |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
129 |
if (id == to_id) shifted |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
130 |
else _from_current(to_id, rest_changes, shifted) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
131 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
132 |
} |
34446 | 133 |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
134 |
def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int = |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
135 |
changes match { |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
136 |
case Nil => pos |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
137 |
case Text.Change(id, start, added, removed) :: rest_changes => { |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
138 |
val shifted = if (id == from_id) pos else _to_current(from_id, rest_changes, pos) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
139 |
if (start <= shifted) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
140 |
if (shifted < start + removed) start |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
141 |
else shifted + added.length - removed |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
142 |
else shifted |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
143 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
144 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
145 |
|
34546 | 146 |
def to_current(from_id: String, pos : Int) = |
147 |
_to_current(from_id, if (col == null) changes else col :: changes, pos) |
|
148 |
def from_current(to_id: String, pos : Int) = |
|
149 |
_from_current(to_id, if (col == null) changes else col :: changes, pos) |
|
34446 | 150 |
|
151 |
def repaint(cmd: Command) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
152 |
{ |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
153 |
val document = prover.document |
34507 | 154 |
if (text_area != null) { |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
155 |
val start = text_area.getLineOfOffset(to_current(document.id, cmd.start)) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
156 |
val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
157 |
text_area.invalidateLineRange(start, stop) |
34446 | 158 |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
159 |
if (Isabelle.prover_setup(buffer).get.selected_state == cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
160 |
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
|
161 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
162 |
} |
34446 | 163 |
|
164 |
def repaint_all() = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
165 |
{ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
166 |
if (text_area != null) |
34446 | 167 |
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
|
168 |
} |
34391 | 169 |
|
34446 | 170 |
def encolor(gfx: Graphics2D, |
171 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) = |
|
172 |
{ |
|
173 |
val start = text_area.offsetToXY(begin) |
|
174 |
val stop = |
|
175 |
if (finish < buffer.getLength) text_area.offsetToXY(finish) |
|
176 |
else { |
|
177 |
val p = text_area.offsetToXY(finish - 1) |
|
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
178 |
val metrics = text_area.getPainter.getFontMetrics |
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
179 |
p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) |
34446 | 180 |
p |
34391 | 181 |
} |
34446 | 182 |
|
183 |
if (start != null && stop != null) { |
|
184 |
gfx.setColor(color) |
|
185 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
|
186 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
|
187 |
} |
|
34391 | 188 |
} |
189 |
||
34446 | 190 |
|
191 |
/* TextAreaExtension methods */ |
|
192 |
||
193 |
override def paintValidLine(gfx: Graphics2D, |
|
34450 | 194 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) = |
34446 | 195 |
{ |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
196 |
val document = prover.document |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
197 |
def from_current(pos: Int) = this.from_current(document.id, pos) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
198 |
def to_current(pos: Int) = this.to_current(document.id, pos) |
34446 | 199 |
val saved_color = gfx.getColor |
200 |
||
201 |
val metrics = text_area.getPainter.getFontMetrics |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
202 |
var e = document.find_command_at(from_current(start)) |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
203 |
val commands = document.commands.dropWhile(_.stop <= from_current(start)). |
34526 | 204 |
takeWhile(c => to_current(c.start) < end) |
34446 | 205 |
// encolor phase |
34526 | 206 |
for (e <- commands) { |
34446 | 207 |
val begin = start max to_current(e.start) |
208 |
val finish = end - 1 min to_current(e.stop) |
|
209 |
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true) |
|
210 |
||
34391 | 211 |
// paint details of command |
34446 | 212 |
for (node <- e.root_node.dfs) { |
213 |
val begin = to_current(node.start + e.start) |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34513
diff
changeset
|
214 |
val finish = to_current(node.stop + e.start) |
34446 | 215 |
if (finish > start && begin < end) { |
34517 | 216 |
encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1, |
217 |
DynamicTokenMarker.choose_color(node.kind), true) |
|
34446 | 218 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
219 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
220 |
} |
34391 | 221 |
|
34446 | 222 |
gfx.setColor(saved_color) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
223 |
} |
34446 | 224 |
|
225 |
/* BufferListener methods */ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
226 |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
227 |
private var changes: List[Text.Change] = Nil |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
228 |
|
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
229 |
private def commit { |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
230 |
if (col != null) { |
34546 | 231 |
changes = col :: changes |
34532 | 232 |
document_actor ! col |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
233 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
234 |
col = null |
34446 | 235 |
if (col_timer.isRunning()) |
236 |
col_timer.stop() |
|
237 |
} |
|
238 |
||
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
239 |
private def delay_commit { |
34446 | 240 |
if (col_timer.isRunning()) |
241 |
col_timer.restart() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
242 |
else |
34446 | 243 |
col_timer.start() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
244 |
} |
34446 | 245 |
|
246 |
||
247 |
override def contentInserted(buffer: JEditBuffer, |
|
248 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
|
249 |
||
250 |
override def contentRemoved(buffer: JEditBuffer, |
|
251 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
252 |
|
34446 | 253 |
override def preContentInserted(buffer: JEditBuffer, |
254 |
start_line: Int, offset: Int, num_lines: Int, length: Int) = |
|
255 |
{ |
|
34526 | 256 |
val text = buffer.getText(offset, length) |
34364 | 257 |
if (col == null) |
34541 | 258 |
col = new Text.Change(id(), offset, text, 0) |
34526 | 259 |
else if (col.start <= offset && offset <= col.start + col.added.length) |
34541 | 260 |
col = new Text.Change(col.id, col.start, col.added + text, col.removed) |
34446 | 261 |
else { |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
262 |
commit |
34541 | 263 |
col = new Text.Change(id(), offset, text, 0) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
264 |
} |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
265 |
delay_commit |
34446 | 266 |
} |
267 |
||
268 |
override def preContentRemoved(buffer: JEditBuffer, |
|
269 |
start_line: Int, start: Int, num_lines: Int, removed: Int) = |
|
270 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
271 |
if (col == null) |
34541 | 272 |
col = new Text.Change(id(), start, "", removed) |
34526 | 273 |
else if (col.start > start + removed || start > col.start + col.added.length) { |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
274 |
commit |
34541 | 275 |
col = new Text.Change(id(), start, "", removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
276 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
277 |
else { |
34526 | 278 |
/* val offset = start - col.start |
279 |
val diff = col.added.length - removed |
|
34446 | 280 |
val (added, add_removed) = |
281 |
if (diff < offset) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
282 |
(offset max 0, diff - (offset max 0)) |
34446 | 283 |
else |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
284 |
(diff - (offset min 0), offset min 0) |
34526 | 285 |
col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/ |
286 |
commit |
|
34541 | 287 |
col = new Text.Change(id(), start, "", removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
288 |
} |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
289 |
delay_commit |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
290 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
291 |
|
34446 | 292 |
override def bufferLoaded(buffer: JEditBuffer) { } |
293 |
override def foldHandlerChanged(buffer: JEditBuffer) { } |
|
294 |
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } |
|
295 |
override def transactionComplete(buffer: JEditBuffer) { } |
|
34447 | 296 |
} |