author | wenzelm |
Tue, 08 Dec 2009 23:45:42 +0100 | |
changeset 34773 | bb5d68f7fd5e |
parent 34772 | 1a79c9b9af82 |
child 34777 | 91d6089cef88 |
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 |
||
34760 | 9 |
package isabelle.proofdocument |
10 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
34703 | 12 |
import scala.actors.Actor, Actor._ |
34693 | 13 |
import scala.collection.mutable |
34446 | 14 |
|
34703 | 15 |
import java.awt.{Color, Graphics2D} |
34447 | 16 |
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
|
17 |
|
34446 | 18 |
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer} |
19 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} |
|
34649 | 20 |
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
|
21 |
|
34773 | 22 |
import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker} |
34446 | 23 |
|
34760 | 24 |
|
25 |
object Theory_View |
|
34588 | 26 |
{ |
34760 | 27 |
def choose_color(command: Command, doc: Proof_Document): Color = |
34716 | 28 |
{ |
29 |
command.status(doc) match { |
|
34653 | 30 |
case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
31 |
case Command.Status.FINISHED => new Color(234, 248, 255) |
|
34716 | 32 |
case Command.Status.FAILED => new Color(255, 106, 106) |
34653 | 33 |
case _ => Color.red |
34 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
} |
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 |
|
34446 | 38 |
|
34760 | 39 |
class Theory_View(text_area: JEditTextArea) |
34588 | 40 |
{ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
41 |
private val buffer = text_area.getBuffer |
34672 | 42 |
|
34719
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
43 |
|
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
44 |
/* prover setup */ |
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
45 |
|
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
46 |
val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic()) |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
47 |
|
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
48 |
prover.command_change += ((command: Command) => |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
49 |
if (current_document().commands.contains(command)) |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
50 |
Swing_Thread.later { |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
51 |
// FIXME proper handling of buffer vs. text areas |
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
52 |
// repaint if buffer is active |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
53 |
if (text_area.getBuffer == buffer) { |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
54 |
update_syntax(command) |
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
55 |
invalidate_line(command) |
34736 | 56 |
overview.repaint() |
34719
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
57 |
} |
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34719
diff
changeset
|
58 |
}) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
59 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
60 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
61 |
/* changes vs. edits */ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
62 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
63 |
private val change_0 = new Change(prover.document_0.id, None, Nil) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
64 |
private var _changes = List(change_0) // owned by Swing/AWT thread |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
65 |
def changes = _changes |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
66 |
private var current_change = change_0 |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
67 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
68 |
private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
69 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
70 |
private val edits_delay = Swing_Thread.delay_last(300) { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
71 |
if (!edits.isEmpty) { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
72 |
val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
73 |
_changes ::= change |
34742 | 74 |
prover.input(change) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
75 |
current_change = change |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
76 |
edits.clear |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
77 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
78 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
79 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
80 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
81 |
/* buffer_listener */ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
82 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
83 |
private val buffer_listener = new BufferListener { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
84 |
override def preContentInserted(buffer: JEditBuffer, |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
85 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
86 |
{ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
87 |
edits += Insert(offset, buffer.getText(offset, length)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
88 |
edits_delay() |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
89 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
90 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
91 |
override def preContentRemoved(buffer: JEditBuffer, |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
92 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
93 |
{ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
94 |
edits += Remove(start, buffer.getText(start, removed_length)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
95 |
edits_delay() |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
96 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
97 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
98 |
override def contentInserted(buffer: JEditBuffer, |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
99 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
100 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
101 |
override def contentRemoved(buffer: JEditBuffer, |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
102 |
start_line: Int, offset: Int, num_lines: Int, length: Int) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
103 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
104 |
override def bufferLoaded(buffer: JEditBuffer) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
105 |
override def foldHandlerChanged(buffer: JEditBuffer) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
106 |
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
107 |
override def transactionComplete(buffer: JEditBuffer) { } |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
108 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
109 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
110 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
111 |
/* text_area_extension */ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
112 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
113 |
private val text_area_extension = new TextAreaExtension { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
114 |
override def paintValidLine(gfx: Graphics2D, |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
115 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
116 |
{ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
117 |
val document = current_document() |
34760 | 118 |
def from_current(pos: Int) = Theory_View.this.from_current(document, pos) |
119 |
def to_current(pos: Int) = Theory_View.this.to_current(document, pos) |
|
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
120 |
val saved_color = gfx.getColor |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
121 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
122 |
val metrics = text_area.getPainter.getFontMetrics |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
123 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
124 |
// encolor phase |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
125 |
var cmd = document.command_at(from_current(start)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
126 |
while (cmd.isDefined && cmd.get.start(document) < end) { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
127 |
val e = cmd.get |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
128 |
val begin = start max to_current(e.start(document)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
129 |
val finish = (end - 1) min to_current(e.stop(document)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
130 |
encolor(gfx, y, metrics.getHeight, begin, finish, |
34760 | 131 |
Theory_View.choose_color(e, document), true) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
132 |
cmd = document.commands.next(e) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
133 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
134 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
135 |
gfx.setColor(saved_color) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
136 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
137 |
|
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
138 |
override def getToolTipText(x: Int, y: Int): String = |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
139 |
{ |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
140 |
val document = current_document() |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
141 |
val offset = from_current(document, text_area.xyToOffset(x, y)) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
142 |
document.command_at(offset) match { |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
143 |
case Some(cmd) => |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
144 |
document.token_start(cmd.tokens.first) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
145 |
cmd.type_at(document, offset - cmd.start(document)).getOrElse(null) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
146 |
case None => null |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
147 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
148 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
149 |
} |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
150 |
|
34446 | 151 |
|
34680 | 152 |
/* activation */ |
34446 | 153 |
|
34736 | 154 |
private val overview = new Document_Overview(prover, text_area, to_current) |
34446 | 155 |
|
156 |
private val selected_state_controller = new CaretListener { |
|
34719
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
157 |
override def caretUpdate(e: CaretEvent) { |
34650 | 158 |
val doc = current_document() |
34712
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
159 |
doc.command_at(e.getDot) match { |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
160 |
case Some(cmd) |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
161 |
if (doc.token_start(cmd.tokens.first) <= e.getDot && |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
162 |
Isabelle.plugin.selected_state != cmd) => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
163 |
Isabelle.plugin.selected_state = cmd |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
164 |
case _ => |
4f0ee5ab0380
replaced find_command_at by command_at -- null-free, proper Option;
wenzelm
parents:
34709
diff
changeset
|
165 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
166 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
167 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
168 |
|
34760 | 169 |
def activate() |
170 |
{ |
|
34446 | 171 |
text_area.addCaretListener(selected_state_controller) |
34736 | 172 |
text_area.addLeftOfScrollBar(overview) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
173 |
text_area.getPainter. |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
174 |
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) |
34760 | 175 |
buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover)) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
176 |
buffer.addBufferListener(buffer_listener) |
34671 | 177 |
buffer.propertiesChanged() |
34446 | 178 |
} |
179 |
||
34772 | 180 |
def deactivate() |
181 |
{ |
|
34649 | 182 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
183 |
buffer.removeBufferListener(buffer_listener) |
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
184 |
text_area.getPainter.removeExtension(text_area_extension) |
34736 | 185 |
text_area.removeLeftOfScrollBar(overview) |
34446 | 186 |
text_area.removeCaretListener(selected_state_controller) |
187 |
} |
|
188 |
||
189 |
||
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
190 |
/* history of changes */ |
34660 | 191 |
|
34760 | 192 |
private def doc_or_pred(c: Change): Proof_Document = |
34660 | 193 |
prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
194 |
|
34654 | 195 |
def current_document() = doc_or_pred(current_change) |
196 |
||
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
197 |
|
34654 | 198 |
/* update to desired version */ |
199 |
||
34660 | 200 |
def set_version(goal: Change) { |
34654 | 201 |
// changes in buffer must be ignored |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
202 |
buffer.removeBufferListener(buffer_listener) |
34654 | 203 |
|
34693 | 204 |
def apply(change: Change): Unit = change.edits.foreach { |
205 |
case Insert(start, text) => buffer.insert(start, text) |
|
206 |
case Remove(start, text) => buffer.remove(start, text.length) |
|
34660 | 207 |
} |
208 |
||
34693 | 209 |
def unapply(change: Change): Unit = change.edits.reverse.foreach { |
210 |
case Insert(start, text) => buffer.remove(start, text.length) |
|
211 |
case Remove(start, text) => buffer.insert(start, text) |
|
34660 | 212 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
213 |
|
34654 | 214 |
// undo/redo changes |
215 |
val ancs_current = current_change.ancestors |
|
216 |
val ancs_goal = goal.ancestors |
|
217 |
val paired = ancs_current.reverse zip ancs_goal.reverse |
|
218 |
def last_common[A](xs: List[(A, A)]): Option[A] = { |
|
219 |
xs match { |
|
220 |
case (x, y) :: xs => |
|
221 |
if (x == y) |
|
222 |
xs match { |
|
223 |
case (a, b) :: ys => |
|
224 |
if (a == b) last_common(xs) |
|
225 |
else Some(x) |
|
226 |
case _ => Some(x) |
|
227 |
} |
|
228 |
else None |
|
229 |
case _ => None |
|
230 |
} |
|
231 |
} |
|
232 |
val common_anc = last_common(paired).get |
|
233 |
||
234 |
ancs_current.takeWhile(_ != common_anc) map unapply |
|
235 |
ancs_goal.takeWhile(_ != common_anc).reverse map apply |
|
236 |
||
237 |
current_change = goal |
|
238 |
// invoke repaint |
|
34679 | 239 |
buffer.propertiesChanged() |
240 |
invalidate_all() |
|
34736 | 241 |
overview.repaint() |
34654 | 242 |
|
34703 | 243 |
// track changes in buffer |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
244 |
buffer.addBufferListener(buffer_listener) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
245 |
} |
34446 | 246 |
|
34693 | 247 |
|
34680 | 248 |
/* transforming offsets */ |
249 |
||
34760 | 250 |
private def changes_from(doc: Proof_Document): List[Edit] = |
34718 | 251 |
List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) ::: |
252 |
edits.toList |
|
34680 | 253 |
|
34760 | 254 |
def from_current(doc: Proof_Document, offset: Int): Int = |
34718 | 255 |
(offset /: changes_from(doc).reverse) ((i, change) => change before i) |
34680 | 256 |
|
34760 | 257 |
def to_current(doc: Proof_Document, offset: Int): Int = |
34718 | 258 |
(offset /: changes_from(doc)) ((i, change) => change after i) |
34680 | 259 |
|
260 |
||
261 |
private def lines_of_command(cmd: Command) = |
|
262 |
{ |
|
263 |
val document = current_document() |
|
34681
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
264 |
(buffer.getLineOfOffset(to_current(document, cmd.start(document))), |
74cc10b5ba51
fixed some issues with multiple active buffers
immler@in.tum.de
parents:
34680
diff
changeset
|
265 |
buffer.getLineOfOffset(to_current(document, cmd.stop(document)))) |
34680 | 266 |
} |
267 |
||
268 |
||
269 |
/* (re)painting */ |
|
270 |
||
34694 | 271 |
private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() } |
34680 | 272 |
|
273 |
private def update_syntax(cmd: Command) { |
|
274 |
val (line1, line2) = lines_of_command(cmd) |
|
275 |
if (line2 >= text_area.getFirstLine && |
|
276 |
line1 <= text_area.getFirstLine + text_area.getVisibleLines) |
|
277 |
update_delay() |
|
278 |
} |
|
279 |
||
280 |
private def invalidate_line(cmd: Command) = |
|
281 |
{ |
|
282 |
val (start, stop) = lines_of_command(cmd) |
|
283 |
text_area.invalidateLineRange(start, stop) |
|
284 |
||
285 |
if (Isabelle.plugin.selected_state == cmd) |
|
34741 | 286 |
Isabelle.plugin.selected_state = cmd // update State view |
34680 | 287 |
} |
288 |
||
289 |
private def invalidate_all() = |
|
290 |
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, |
|
291 |
text_area.getLastPhysicalLine) |
|
292 |
||
293 |
private def encolor(gfx: Graphics2D, |
|
294 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) |
|
295 |
{ |
|
296 |
val start = text_area.offsetToXY(begin) |
|
297 |
val stop = |
|
298 |
if (finish < buffer.getLength) text_area.offsetToXY(finish) |
|
299 |
else { |
|
300 |
val p = text_area.offsetToXY(finish - 1) |
|
301 |
val metrics = text_area.getPainter.getFontMetrics |
|
302 |
p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) |
|
303 |
p |
|
304 |
} |
|
305 |
||
306 |
if (start != null && stop != null) { |
|
307 |
gfx.setColor(color) |
|
308 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
|
309 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
|
310 |
} |
|
311 |
} |
|
312 |
||
34696 | 313 |
|
34719
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
314 |
/* init */ |
34680 | 315 |
|
34719
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
316 |
prover.start() |
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
317 |
|
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
318 |
edits += Insert(0, buffer.getText(0, buffer.getLength)) |
f5b408849dcc
eliminated ProverEvents.Activate -- handle "ready" within Prover;
wenzelm
parents:
34718
diff
changeset
|
319 |
edits_delay() |
34447 | 320 |
} |