author | immler@in.tum.de |
Wed, 08 Jul 2009 15:15:15 +0200 | |
changeset 34653 | 2e033aaf128e |
parent 34652 | 5fe5e00ec430 |
child 34654 | 30f588245884 |
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 |
34582 | 12 |
import scala.actors.Actor._ |
34446 | 13 |
|
34653 | 14 |
import isabelle.proofdocument.{ProofDocument, Text} |
34649 | 15 |
import isabelle.prover.{Prover, ProverEvents, Command} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
import java.awt.Graphics2D |
34446 | 18 |
import java.awt.event.{ActionEvent, ActionListener} |
19 |
import java.awt.Color |
|
34447 | 20 |
import javax.swing.Timer |
21 |
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
|
22 |
|
34446 | 23 |
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer} |
24 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} |
|
34649 | 25 |
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
26 |
|
34446 | 27 |
|
34588 | 28 |
object TheoryView |
29 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
30 |
|
34574
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
31 |
val MAX_CHANGE_LENGTH = 1500 |
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
32 |
|
34653 | 33 |
def choose_color(cmd: Command, doc: ProofDocument): Color = { |
34 |
cmd.status(doc) match { |
|
35 |
case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
|
36 |
case Command.Status.FINISHED => new Color(234, 248, 255) |
|
37 |
case Command.Status.FAILED => new Color(255, 192, 192) |
|
38 |
case _ => Color.red |
|
39 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
40 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
41 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
42 |
|
34446 | 43 |
|
34532 | 44 |
class TheoryView (text_area: JEditTextArea, document_actor: Actor) |
34588 | 45 |
extends TextAreaExtension with BufferListener |
46 |
{ |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
47 |
|
34603
83a37e3b8c9c
produce ids via Isabelle.system (http://isabelle.in.tum.de/repos/isabelle/rev/c23663825e23);
wenzelm
parents:
34598
diff
changeset
|
48 |
def id() = Isabelle.system.id() |
34541 | 49 |
|
34446 | 50 |
private val buffer = text_area.getBuffer |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
51 |
private val prover = Isabelle.prover_setup(buffer).get.prover |
34446 | 52 |
|
53 |
||
34526 | 54 |
private var col: Text.Change = null |
34650 | 55 |
private var doc_id: IsarDocument.Document_ID = prover.document(null).id |
56 |
def current_document() = prover.document(doc_id) |
|
34446 | 57 |
|
58 |
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
|
59 |
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
|
60 |
}) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
61 |
|
34446 | 62 |
col_timer.stop |
63 |
col_timer.setRepeats(true) |
|
64 |
||
65 |
||
34566 | 66 |
private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current) |
34446 | 67 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
68 |
|
34446 | 69 |
/* activation */ |
70 |
||
71 |
private val selected_state_controller = new CaretListener { |
|
72 |
override def caretUpdate(e: CaretEvent) = { |
|
34650 | 73 |
val doc = current_document() |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
74 |
val cmd = doc.find_command_at(e.getDot) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
75 |
if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot && |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
76 |
Isabelle.prover_setup(buffer).get.selected_state != cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
77 |
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
|
78 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
79 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
80 |
|
34582 | 81 |
def activate() { |
34446 | 82 |
text_area.addCaretListener(selected_state_controller) |
83 |
text_area.addLeftOfScrollBar(phase_overview) |
|
84 |
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
|
85 |
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) |
34649 | 86 |
buffer.addBufferListener(this) |
87 |
||
34650 | 88 |
col = Text.Change(doc_id, Isabelle.system.id(), 0, |
89 |
buffer.getText(0, buffer.getLength), "") |
|
90 |
commit |
|
34446 | 91 |
} |
92 |
||
34582 | 93 |
def deactivate() { |
34649 | 94 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
95 |
buffer.removeBufferListener(this) |
|
34446 | 96 |
text_area.getPainter.removeExtension(this) |
97 |
text_area.removeLeftOfScrollBar(phase_overview) |
|
98 |
text_area.removeCaretListener(selected_state_controller) |
|
99 |
} |
|
100 |
||
101 |
||
102 |
/* painting */ |
|
103 |
||
34643
3896caeedf82
renamed Delay to clarified version Swing_Thread.delay;
wenzelm
parents:
34642
diff
changeset
|
104 |
val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() } |
3896caeedf82
renamed Delay to clarified version Swing_Thread.delay;
wenzelm
parents:
34642
diff
changeset
|
105 |
val repaint_delay = Swing_Thread.delay(100){ repaint_all() } |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
106 |
|
34582 | 107 |
val change_receiver = actor { |
108 |
loop { |
|
109 |
react { |
|
34649 | 110 |
case ProverEvents.Activate => |
111 |
activate() |
|
112 |
case c: Command => |
|
34643
3896caeedf82
renamed Delay to clarified version Swing_Thread.delay;
wenzelm
parents:
34642
diff
changeset
|
113 |
update_delay() |
3896caeedf82
renamed Delay to clarified version Swing_Thread.delay;
wenzelm
parents:
34642
diff
changeset
|
114 |
repaint_delay() |
3896caeedf82
renamed Delay to clarified version Swing_Thread.delay;
wenzelm
parents:
34642
diff
changeset
|
115 |
phase_overview.repaint_delay() |
34649 | 116 |
case x => System.err.println("warning: change_receiver ignored " + x) |
34538
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 |
} |
34583
17c83413b7fe
change_receiver: start only once (already done in actor function);
wenzelm
parents:
34582
diff
changeset
|
119 |
} |
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 |
34650 | 124 |
case Text.Change(_, id, start, added, removed) :: rest_changes => { |
34582 | 125 |
val shifted = |
126 |
if (start <= pos) |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
127 |
if (pos < start + added.length) start |
34648 | 128 |
else pos - added.length + removed.length |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
129 |
else pos |
34547 | 130 |
if (id == to_id) pos |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
131 |
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
|
132 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
133 |
} |
34446 | 134 |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
135 |
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
|
136 |
changes match { |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
137 |
case Nil => pos |
34650 | 138 |
case Text.Change(_, id, start, added, removed) :: rest_changes => { |
34547 | 139 |
val shifted = _to_current(from_id, rest_changes, pos) |
140 |
if (id == from_id) pos |
|
141 |
else if (start <= shifted) { |
|
34648 | 142 |
if (shifted < start + removed.length) start |
143 |
else shifted + added.length - removed.length |
|
34547 | 144 |
} else shifted |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
145 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
146 |
} |
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
147 |
|
34651
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
148 |
def to_current(from_id: String, pos: Int) = _to_current(from_id, |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
149 |
if (col == null) current_changes else col :: current_changes, pos) |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
150 |
def from_current(to_id: String, pos: Int) = _from_current(to_id, |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
151 |
if (col == null) current_changes else col :: current_changes, pos) |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
152 |
def to_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int = |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
153 |
to_current(doc.id, pos) |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
154 |
def from_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int = |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
155 |
from_current(doc.id, pos) |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
156 |
|
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
157 |
/* update to desired version */ |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
158 |
|
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
159 |
def set_version(id: String) { |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
160 |
// changes in buffer must be ignored |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
161 |
buffer.removeBufferListener(this) |
34652
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
162 |
|
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
163 |
val base = changes.find(_.id == doc_id).get |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
164 |
val goal = changes.find(_.id == id).get |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
165 |
|
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
166 |
if (changes.indexOf(base) < changes.indexOf(goal)) |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
167 |
changes.dropWhile(_ != base).takeWhile(_ != goal).map { c => |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
168 |
buffer.remove(c.start, c.added.length) |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
169 |
buffer.insert(c.start, c.removed)} |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
170 |
else |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
171 |
changes.dropWhile(_ != goal).takeWhile(_ != base).reverse.map { c => |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
172 |
buffer.remove(c.start, c.removed.length) |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
173 |
buffer.insert(c.start, c.added)} |
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
174 |
|
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
175 |
val content = buffer.getText(0, buffer.getLength) |
34651
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
176 |
doc_id = id |
34653 | 177 |
// invoke repaint |
178 |
update_delay() |
|
179 |
repaint_delay() |
|
180 |
phase_overview.repaint_delay() |
|
181 |
||
34651
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
182 |
buffer.addBufferListener(this) |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
183 |
} |
34446 | 184 |
|
185 |
def repaint(cmd: Command) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
186 |
{ |
34650 | 187 |
val document = current_document() |
34507 | 188 |
if (text_area != null) { |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
189 |
val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document))) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
190 |
val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
191 |
text_area.invalidateLineRange(start, stop) |
34446 | 192 |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
193 |
if (Isabelle.prover_setup(buffer).get.selected_state == cmd) |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34458
diff
changeset
|
194 |
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
|
195 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
196 |
} |
34446 | 197 |
|
34588 | 198 |
def repaint_all() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
199 |
{ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
200 |
if (text_area != null) |
34446 | 201 |
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
|
202 |
} |
34391 | 203 |
|
34446 | 204 |
def encolor(gfx: Graphics2D, |
34588 | 205 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) |
34446 | 206 |
{ |
207 |
val start = text_area.offsetToXY(begin) |
|
208 |
val stop = |
|
209 |
if (finish < buffer.getLength) text_area.offsetToXY(finish) |
|
210 |
else { |
|
211 |
val p = text_area.offsetToXY(finish - 1) |
|
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
212 |
val metrics = text_area.getPainter.getFontMetrics |
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
213 |
p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) |
34446 | 214 |
p |
34391 | 215 |
} |
34446 | 216 |
|
217 |
if (start != null && stop != null) { |
|
218 |
gfx.setColor(color) |
|
219 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
|
220 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
|
221 |
} |
|
34391 | 222 |
} |
223 |
||
34446 | 224 |
|
225 |
/* TextAreaExtension methods */ |
|
226 |
||
227 |
override def paintValidLine(gfx: Graphics2D, |
|
34588 | 228 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
34446 | 229 |
{ |
34650 | 230 |
val document = current_document() |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
231 |
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
|
232 |
def to_current(pos: Int) = this.to_current(document.id, pos) |
34446 | 233 |
val saved_color = gfx.getColor |
234 |
||
235 |
val metrics = text_area.getPainter.getFontMetrics |
|
34596 | 236 |
|
237 |
// encolor phase |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
238 |
var e = document.find_command_at(from_current(start)) |
34596 | 239 |
while (e != null && e.start(document) < end) { |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
240 |
val begin = start max to_current(e.start(document)) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
241 |
val finish = end - 1 min to_current(e.stop(document)) |
34653 | 242 |
encolor(gfx, y, metrics.getHeight, begin, finish, |
243 |
TheoryView.choose_color(e, document), true) |
|
34596 | 244 |
e = document.commands.next(e).getOrElse(null) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
245 |
} |
34391 | 246 |
|
34446 | 247 |
gfx.setColor(saved_color) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
248 |
} |
34446 | 249 |
|
34562 | 250 |
override def getToolTipText(x: Int, y: Int) = { |
34650 | 251 |
val document = current_document() |
34562 | 252 |
val offset = from_current(document.id, text_area.xyToOffset(x, y)) |
253 |
val cmd = document.find_command_at(offset) |
|
254 |
if (cmd != null) { |
|
255 |
document.token_start(cmd.tokens.first) |
|
34653 | 256 |
cmd.type_at(document, offset - cmd.start(document)) |
34562 | 257 |
} else null |
258 |
} |
|
259 |
||
34446 | 260 |
/* BufferListener methods */ |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
261 |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
262 |
private var changes: List[Text.Change] = Nil |
34651
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
263 |
private def current_changes = changes.dropWhile(_.id != doc_id) |
34652
5fe5e00ec430
gui element to set current document version
immler@in.tum.de
parents:
34651
diff
changeset
|
264 |
def get_changes = changes |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
265 |
|
34547 | 266 |
private def commit: Unit = synchronized { |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
267 |
if (col != null) { |
34574
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
268 |
def split_changes(c: Text.Change): List[Text.Change] = { |
34582 | 269 |
val MAX = TheoryView.MAX_CHANGE_LENGTH |
270 |
if (c.added.length <= MAX) List(c) |
|
34650 | 271 |
else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) :: |
272 |
split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), "")) |
|
34574
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
273 |
} |
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
274 |
val new_changes = split_changes(col) |
34651
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
275 |
changes = new_changes.reverse ::: current_changes |
23271beee68a
set current document version; forget "future" versions in list
immler@in.tum.de
parents:
34650
diff
changeset
|
276 |
doc_id = new_changes.head.id |
34574
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
277 |
new_changes map (document_actor ! _) |
34650 | 278 |
doc_id = new_changes.last.id |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
279 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
280 |
col = null |
34446 | 281 |
if (col_timer.isRunning()) |
282 |
col_timer.stop() |
|
283 |
} |
|
284 |
||
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
285 |
private def delay_commit { |
34446 | 286 |
if (col_timer.isRunning()) |
287 |
col_timer.restart() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
288 |
else |
34446 | 289 |
col_timer.start() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
290 |
} |
34446 | 291 |
|
292 |
||
293 |
override def contentInserted(buffer: JEditBuffer, |
|
294 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
|
295 |
||
296 |
override def contentRemoved(buffer: JEditBuffer, |
|
297 |
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
|
298 |
|
34446 | 299 |
override def preContentInserted(buffer: JEditBuffer, |
34588 | 300 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
34446 | 301 |
{ |
34526 | 302 |
val text = buffer.getText(offset, length) |
34364 | 303 |
if (col == null) |
34650 | 304 |
col = new Text.Change(doc_id, id(), offset, text, "") |
34526 | 305 |
else if (col.start <= offset && offset <= col.start + col.added.length) |
34650 | 306 |
col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed) |
34446 | 307 |
else { |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
308 |
commit |
34650 | 309 |
col = new Text.Change(doc_id, id(), offset, text, "") |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
310 |
} |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
311 |
delay_commit |
34446 | 312 |
} |
313 |
||
314 |
override def preContentRemoved(buffer: JEditBuffer, |
|
34648 | 315 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
34446 | 316 |
{ |
34648 | 317 |
val removed = buffer.getText(start, removed_length) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
318 |
if (col == null) |
34650 | 319 |
col = new Text.Change(doc_id, id(), start, "", removed) |
34648 | 320 |
else if (col.start > start + removed_length || start > col.start + col.added.length) { |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
321 |
commit |
34650 | 322 |
col = new Text.Change(doc_id, id(), start, "", removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
323 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
324 |
else { |
34526 | 325 |
/* val offset = start - col.start |
326 |
val diff = col.added.length - removed |
|
34446 | 327 |
val (added, add_removed) = |
328 |
if (diff < offset) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
329 |
(offset max 0, diff - (offset max 0)) |
34446 | 330 |
else |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
331 |
(diff - (offset min 0), offset min 0) |
34526 | 332 |
col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/ |
333 |
commit |
|
34650 | 334 |
col = new Text.Change(doc_id, id(), start, "", removed) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
335 |
} |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
336 |
delay_commit |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
337 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
338 |
|
34446 | 339 |
override def bufferLoaded(buffer: JEditBuffer) { } |
340 |
override def foldHandlerChanged(buffer: JEditBuffer) { } |
|
341 |
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } |
|
342 |
override def transactionComplete(buffer: JEditBuffer) { } |
|
34588 | 343 |
|
34447 | 344 |
} |