author | immler@in.tum.de |
Thu, 27 Aug 2009 10:51:09 +0200 | |
changeset 34682 | bcae80cc4170 |
parent 34681 | 74cc10b5ba51 |
child 34685 | 93f4978fe2a8 |
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 |
|
34660 | 14 |
import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove} |
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 |
{ |
|
34574
d68352286c91
split large changes for faster responses of prover
immler@in.tum.de
parents:
34568
diff
changeset
|
30 |
|
34653 | 31 |
def choose_color(cmd: Command, doc: ProofDocument): Color = { |
32 |
cmd.status(doc) match { |
|
33 |
case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
|
34 |
case Command.Status.FINISHED => new Color(234, 248, 255) |
|
35 |
case Command.Status.FAILED => new Color(255, 192, 192) |
|
36 |
case _ => Color.red |
|
37 |
} |
|
34318
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 |
|
34672 | 42 |
class TheoryView (text_area: JEditTextArea) |
34588 | 43 |
extends TextAreaExtension with BufferListener |
44 |
{ |
|
34541 | 45 |
|
34680 | 46 |
val buffer = text_area.getBuffer |
34672 | 47 |
|
48 |
// start prover |
|
49 |
val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic, change_receiver) |
|
50 |
prover.start() // start actor |
|
34446 | 51 |
|
52 |
||
34680 | 53 |
/* activation */ |
34446 | 54 |
|
34566 | 55 |
private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current) |
34446 | 56 |
|
57 |
private val selected_state_controller = new CaretListener { |
|
58 |
override def caretUpdate(e: CaretEvent) = { |
|
34650 | 59 |
val doc = current_document() |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34549
diff
changeset
|
60 |
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
|
61 |
if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot && |
34669 | 62 |
Isabelle.plugin.selected_state != cmd) |
63 |
Isabelle.plugin.selected_state = cmd |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
64 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
65 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
66 |
|
34582 | 67 |
def activate() { |
34446 | 68 |
text_area.addCaretListener(selected_state_controller) |
69 |
text_area.addLeftOfScrollBar(phase_overview) |
|
70 |
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
|
71 |
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) |
34649 | 72 |
buffer.addBufferListener(this) |
34671 | 73 |
|
74 |
val dockable = |
|
75 |
text_area.getView.getDockableWindowManager.getDockable("isabelle-output") |
|
76 |
if (dockable != null) { |
|
77 |
val output_dockable = dockable.asInstanceOf[OutputDockable] |
|
78 |
val output_text_view = prover.output_text_view |
|
79 |
output_dockable.set_text(output_text_view) |
|
80 |
} |
|
81 |
||
82 |
buffer.propertiesChanged() |
|
34446 | 83 |
} |
84 |
||
34582 | 85 |
def deactivate() { |
34649 | 86 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
87 |
buffer.removeBufferListener(this) |
|
34446 | 88 |
text_area.getPainter.removeExtension(this) |
89 |
text_area.removeLeftOfScrollBar(phase_overview) |
|
90 |
text_area.removeCaretListener(selected_state_controller) |
|
91 |
} |
|
92 |
||
93 |
||
34654 | 94 |
/* history of changes - TODO: seperate class?*/ |
95 |
||
34680 | 96 |
private val change_0 = new Change(prover.document_0.id, None, Nil) |
97 |
private var _changes = List(change_0) |
|
98 |
def changes = _changes |
|
34654 | 99 |
private var current_change = change_0 |
34660 | 100 |
|
101 |
private def doc_or_pred(c: Change): ProofDocument = |
|
102 |
prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) |
|
34654 | 103 |
def current_document() = doc_or_pred(current_change) |
104 |
||
105 |
/* update to desired version */ |
|
106 |
||
34660 | 107 |
def set_version(goal: Change) { |
34654 | 108 |
// changes in buffer must be ignored |
109 |
buffer.removeBufferListener(this) |
|
110 |
||
34660 | 111 |
def apply(c: Change) = c.map { |
112 |
case Insert(start, added) => buffer.insert(start, added) |
|
113 |
case Remove(start, removed) => buffer.remove(start, removed.length) |
|
114 |
} |
|
115 |
||
34682 | 116 |
def unapply(c: Change) = c.toList.reverse.map { |
34660 | 117 |
case Insert(start, added) => buffer.remove(start, added.length) |
118 |
case Remove(start, removed) => buffer.insert(start, removed) |
|
119 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
120 |
|
34654 | 121 |
// undo/redo changes |
122 |
val ancs_current = current_change.ancestors |
|
123 |
val ancs_goal = goal.ancestors |
|
124 |
val paired = ancs_current.reverse zip ancs_goal.reverse |
|
125 |
def last_common[A](xs: List[(A, A)]): Option[A] = { |
|
126 |
xs match { |
|
127 |
case (x, y) :: xs => |
|
128 |
if (x == y) |
|
129 |
xs match { |
|
130 |
case (a, b) :: ys => |
|
131 |
if (a == b) last_common(xs) |
|
132 |
else Some(x) |
|
133 |
case _ => Some(x) |
|
134 |
} |
|
135 |
else None |
|
136 |
case _ => None |
|
137 |
} |
|
138 |
} |
|
139 |
val common_anc = last_common(paired).get |
|
140 |
||
141 |
ancs_current.takeWhile(_ != common_anc) map unapply |
|
142 |
ancs_goal.takeWhile(_ != common_anc).reverse map apply |
|
143 |
||
144 |
current_change = goal |
|
145 |
// invoke repaint |
|
34679 | 146 |
buffer.propertiesChanged() |
147 |
invalidate_all() |
|
148 |
phase_overview.repaint() |
|
34654 | 149 |
|
150 |
//track changes in buffer |
|
151 |
buffer.addBufferListener(this) |
|
152 |
} |
|
153 |
||
34680 | 154 |
/* sending edits to prover */ |
155 |
||
156 |
private var edits: List[Edit] = Nil |
|
157 |
||
158 |
private val col_timer = new Timer(300, new ActionListener() { |
|
159 |
override def actionPerformed(e: ActionEvent) = commit |
|
160 |
}) |
|
161 |
||
162 |
col_timer.stop |
|
163 |
col_timer.setRepeats(true) |
|
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
164 |
|
34547 | 165 |
private def commit: Unit = synchronized { |
34660 | 166 |
if (!edits.isEmpty) { |
167 |
val change = new Change(Isabelle.system.id(), Some(current_change), edits) |
|
34680 | 168 |
_changes ::= change |
34672 | 169 |
prover ! change |
34660 | 170 |
current_change = change |
34545
b928628742ed
implemented to_current and from_current in dependancy of document-versions
immler@in.tum.de
parents:
34544
diff
changeset
|
171 |
} |
34660 | 172 |
edits = Nil |
34446 | 173 |
if (col_timer.isRunning()) |
174 |
col_timer.stop() |
|
175 |
} |
|
176 |
||
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
177 |
private def delay_commit { |
34446 | 178 |
if (col_timer.isRunning()) |
179 |
col_timer.restart() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
180 |
else |
34446 | 181 |
col_timer.start() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
182 |
} |
34446 | 183 |
|
34680 | 184 |
/* BufferListener methods */ |
34446 | 185 |
|
186 |
override def contentInserted(buffer: JEditBuffer, |
|
187 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
|
188 |
||
189 |
override def contentRemoved(buffer: JEditBuffer, |
|
190 |
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
|
191 |
|
34446 | 192 |
override def preContentInserted(buffer: JEditBuffer, |
34588 | 193 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
34446 | 194 |
{ |
34660 | 195 |
edits ::= Insert(offset, buffer.getText(offset, length)) |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
196 |
delay_commit |
34446 | 197 |
} |
198 |
||
199 |
override def preContentRemoved(buffer: JEditBuffer, |
|
34648 | 200 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
34446 | 201 |
{ |
34660 | 202 |
edits ::= Remove(start, buffer.getText(start, removed_length)) |
34515
3be515f1379d
use FontMetrics.getMaxAdvance if available; tuned
immler@in.tum.de
parents:
34514
diff
changeset
|
203 |
delay_commit |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
204 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
205 |
|
34446 | 206 |
override def bufferLoaded(buffer: JEditBuffer) { } |
207 |
override def foldHandlerChanged(buffer: JEditBuffer) { } |
|
208 |
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } |
|
209 |
override def transactionComplete(buffer: JEditBuffer) { } |
|
34588 | 210 |
|
34680 | 211 |
|
212 |
/* transforming offsets */ |
|
213 |
||
214 |
private def changes_to(doc: ProofDocument) = |
|
215 |
edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList) |
|
216 |
||
217 |
def from_current(doc: ProofDocument, pos: Int) = |
|
218 |
(pos /: changes_to(doc)) ((p, c) => c from_where p) |
|
219 |
||
220 |
def to_current(doc: ProofDocument, pos: Int) = |
|
221 |
(pos /: changes_to(doc).reverse) ((p, c) => c where_to p) |
|
222 |
||
223 |
||
224 |
private def lines_of_command(cmd: Command) = |
|
225 |
{ |
|
226 |
val document = current_document() |
|
34681
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
227 |
(buffer.getLineOfOffset(to_current(document, cmd.start(document))), |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
228 |
buffer.getLineOfOffset(to_current(document, cmd.stop(document)))) |
34680 | 229 |
} |
230 |
||
231 |
||
232 |
/* (re)painting */ |
|
233 |
||
234 |
private val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() } |
|
235 |
||
236 |
private def update_syntax(cmd: Command) { |
|
237 |
val (line1, line2) = lines_of_command(cmd) |
|
238 |
if (line2 >= text_area.getFirstLine && |
|
239 |
line1 <= text_area.getFirstLine + text_area.getVisibleLines) |
|
240 |
update_delay() |
|
241 |
} |
|
242 |
||
243 |
private def invalidate_line(cmd: Command) = |
|
244 |
{ |
|
245 |
val (start, stop) = lines_of_command(cmd) |
|
246 |
text_area.invalidateLineRange(start, stop) |
|
247 |
||
248 |
if (Isabelle.plugin.selected_state == cmd) |
|
249 |
Isabelle.plugin.selected_state = cmd // update State view |
|
250 |
} |
|
251 |
||
252 |
private def invalidate_all() = |
|
253 |
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, |
|
254 |
text_area.getLastPhysicalLine) |
|
255 |
||
256 |
private def encolor(gfx: Graphics2D, |
|
257 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) |
|
258 |
{ |
|
259 |
val start = text_area.offsetToXY(begin) |
|
260 |
val stop = |
|
261 |
if (finish < buffer.getLength) text_area.offsetToXY(finish) |
|
262 |
else { |
|
263 |
val p = text_area.offsetToXY(finish - 1) |
|
264 |
val metrics = text_area.getPainter.getFontMetrics |
|
265 |
p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) |
|
266 |
p |
|
267 |
} |
|
268 |
||
269 |
if (start != null && stop != null) { |
|
270 |
gfx.setColor(color) |
|
271 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
|
272 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
|
273 |
} |
|
274 |
} |
|
275 |
||
276 |
/* TextAreaExtension methods */ |
|
277 |
||
278 |
override def paintValidLine(gfx: Graphics2D, |
|
279 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
|
280 |
{ |
|
281 |
val document = current_document() |
|
282 |
def from_current(pos: Int) = this.from_current(document, pos) |
|
283 |
def to_current(pos: Int) = this.to_current(document, pos) |
|
284 |
val saved_color = gfx.getColor |
|
285 |
||
286 |
val metrics = text_area.getPainter.getFontMetrics |
|
287 |
||
288 |
// encolor phase |
|
289 |
var e = document.find_command_at(from_current(start)) |
|
290 |
while (e != null && e.start(document) < end) { |
|
291 |
val begin = start max to_current(e.start(document)) |
|
292 |
val finish = end - 1 min to_current(e.stop(document)) |
|
293 |
encolor(gfx, y, metrics.getHeight, begin, finish, |
|
294 |
TheoryView.choose_color(e, document), true) |
|
295 |
e = document.commands.next(e).getOrElse(null) |
|
296 |
} |
|
297 |
||
298 |
gfx.setColor(saved_color) |
|
299 |
} |
|
300 |
||
301 |
override def getToolTipText(x: Int, y: Int) = { |
|
302 |
val document = current_document() |
|
303 |
val offset = from_current(document, text_area.xyToOffset(x, y)) |
|
304 |
val cmd = document.find_command_at(offset) |
|
305 |
if (cmd != null) { |
|
306 |
document.token_start(cmd.tokens.first) |
|
307 |
cmd.type_at(document, offset - cmd.start(document)) |
|
308 |
} else null |
|
309 |
} |
|
310 |
||
311 |
||
312 |
/* receiving from prover */ |
|
313 |
||
314 |
lazy val change_receiver: Actor = actor { |
|
315 |
loop { |
|
316 |
react { |
|
317 |
case ProverEvents.Activate => |
|
318 |
edits = List(Insert(0, buffer.getText(0, buffer.getLength))) |
|
319 |
commit |
|
320 |
case c: Command => |
|
34681
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
321 |
if(current_document().commands.contains(c)) |
34680 | 322 |
Swing_Thread.later { |
34681
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
323 |
// repaint if buffer is active |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
324 |
if(text_area.getBuffer == buffer) { |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
325 |
update_syntax(c) |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
326 |
invalidate_line(c) |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
327 |
phase_overview.repaint() |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
328 |
} |
34680 | 329 |
} |
330 |
case x => System.err.println("warning: change_receiver ignored " + x) |
|
331 |
} |
|
332 |
} |
|
333 |
} |
|
334 |
||
34447 | 335 |
} |