author | wenzelm |
Tue, 15 Dec 2009 20:44:59 +0100 | |
changeset 34789 | 30528e68f774 |
parent 34788 | 3779c54a2d21 |
child 34794 | a4a457e393a4 |
permissions | -rw-r--r-- |
34408 | 1 |
/* |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
2 |
* Document view connected to jEdit text area |
34408 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
5 |
* @author Makarius |
34408 | 6 |
*/ |
7 |
||
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
8 |
package isabelle.jedit |
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
9 |
|
34760 | 10 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
11 |
import isabelle.proofdocument.{Command, Proof_Document, Session} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
12 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
13 |
import scala.actors.Actor._ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
14 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
15 |
import java.awt.event.{MouseAdapter, MouseEvent} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
16 |
import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D} |
34734 | 17 |
import javax.swing.{JPanel, ToolTipManager} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
18 |
import javax.swing.event.{CaretListener, CaretEvent} |
34734 | 19 |
|
34709 | 20 |
import org.gjt.sp.jedit.gui.RolloverButton |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
21 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
22 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
23 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
24 |
object Document_View |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
25 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
26 |
def choose_color(command: Command, doc: Proof_Document): Color = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
27 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
28 |
command.status(doc) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
29 |
case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
30 |
case Command.Status.FINISHED => new Color(234, 248, 255) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
31 |
case Command.Status.FAILED => new Color(255, 106, 106) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
32 |
case _ => Color.red |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
33 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
34 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
35 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
36 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
37 |
/* document view of text area */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
38 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
39 |
private val key = new Object |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
40 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
41 |
def init(model: Document_Model, text_area: TextArea): Document_View = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
42 |
{ |
34789 | 43 |
Swing_Thread.assert() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
44 |
val doc_view = new Document_View(model, text_area) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
45 |
text_area.putClientProperty(key, doc_view) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
46 |
doc_view.activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
47 |
doc_view |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
48 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
49 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
50 |
def apply(text_area: TextArea): Option[Document_View] = |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
51 |
{ |
34789 | 52 |
Swing_Thread.assert() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
53 |
text_area.getClientProperty(key) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
54 |
case doc_view: Document_View => Some(doc_view) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
55 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
56 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
57 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
58 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
59 |
def exit(text_area: TextArea) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
60 |
{ |
34789 | 61 |
Swing_Thread.assert() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
62 |
apply(text_area) match { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
63 |
case None => error("No document view for text area: " + text_area) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
64 |
case Some(doc_view) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
65 |
doc_view.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
66 |
text_area.putClientProperty(key, null) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
67 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
68 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
69 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
70 |
|
34733 | 71 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
72 |
class Document_View(model: Document_Model, text_area: TextArea) |
34654 | 73 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
74 |
private val session = model.session |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
75 |
|
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
76 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
77 |
/* command change actor */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
78 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
79 |
private case object Exit |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
80 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
81 |
private val command_change_actor = actor { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
82 |
loop { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
83 |
react { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
84 |
case command: Command => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
85 |
if (model.current_document().commands.contains(command)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
86 |
Swing_Thread.now { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
87 |
update_syntax(command) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
88 |
invalidate_line(command) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
89 |
overview.repaint() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
90 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
91 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
92 |
case Exit => reply(()); exit() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
93 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
94 |
case bad => System.err.println("command_change_actor: ignoring bad message " + bad) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
95 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
96 |
} |
34678 | 97 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
98 |
|
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
99 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
100 |
/* text_area_extension */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
101 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
102 |
private val text_area_extension = new TextAreaExtension |
34678 | 103 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
104 |
override def paintValidLine(gfx: Graphics2D, |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
105 |
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
106 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
107 |
val document = model.current_document() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
108 |
def from_current(pos: Int) = model.from_current(document, pos) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
109 |
def to_current(pos: Int) = model.to_current(document, pos) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
110 |
val saved_color = gfx.getColor |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
111 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
112 |
val metrics = text_area.getPainter.getFontMetrics |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
113 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
114 |
// encolor phase |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
115 |
var cmd = document.command_at(from_current(start)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
116 |
while (cmd.isDefined && cmd.get.start(document) < end) { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
117 |
val e = cmd.get |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
118 |
val begin = start max to_current(e.start(document)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
119 |
val finish = (end - 1) min to_current(e.stop(document)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
120 |
encolor(gfx, y, metrics.getHeight, begin, finish, |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
121 |
Document_View.choose_color(e, document), true) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
122 |
cmd = document.commands.next(e) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
123 |
} |
34678 | 124 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
125 |
gfx.setColor(saved_color) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
126 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
127 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
128 |
override def getToolTipText(x: Int, y: Int): String = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
129 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
130 |
val document = model.current_document() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
131 |
val offset = model.from_current(document, text_area.xyToOffset(x, y)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
132 |
document.command_at(offset) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
133 |
case Some(cmd) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
134 |
document.token_start(cmd.tokens.first) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
135 |
cmd.type_at(document, offset - cmd.start(document)).getOrElse(null) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
136 |
case None => null |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
137 |
} |
34734 | 138 |
} |
34678 | 139 |
} |
34513 | 140 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
141 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
142 |
/* (re)painting */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
143 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
144 |
private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() } |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
145 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
146 |
private def update_syntax(cmd: Command) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
147 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
148 |
val (line1, line2) = model.lines_of_command(cmd) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
149 |
if (line2 >= text_area.getFirstLine && |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
150 |
line1 <= text_area.getFirstLine + text_area.getVisibleLines) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
151 |
update_delay() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
152 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
153 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
154 |
private def invalidate_line(cmd: Command) = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
155 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
156 |
val (start, stop) = model.lines_of_command(cmd) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
157 |
text_area.invalidateLineRange(start, stop) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
158 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
159 |
if (Isabelle.session.selected_state == cmd) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
160 |
Isabelle.session.selected_state = cmd |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
161 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
162 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
163 |
private def invalidate_all() = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
164 |
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
165 |
text_area.getLastPhysicalLine) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
166 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
167 |
private def encolor(gfx: Graphics2D, |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
168 |
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
169 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
170 |
val start = text_area.offsetToXY(begin) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
171 |
val stop = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
172 |
if (finish < model.buffer.getLength) text_area.offsetToXY(finish) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
173 |
else { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
174 |
val p = text_area.offsetToXY(finish - 1) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
175 |
val metrics = text_area.getPainter.getFontMetrics |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
176 |
p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
177 |
p |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
178 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
179 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
180 |
if (start != null && stop != null) { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
181 |
gfx.setColor(color) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
182 |
if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
183 |
else gfx.drawRect(start.x, y, stop.x - start.x, height) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
184 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
185 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
186 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
187 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
188 |
/* overview of command status left of scrollbar */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
189 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
190 |
val overview = new JPanel(new BorderLayout) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
191 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
192 |
private val WIDTH = 10 |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
193 |
private val HEIGHT = 2 |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
194 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
195 |
setRequestFocusEnabled(false) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
196 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
197 |
addMouseListener(new MouseAdapter { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
198 |
override def mousePressed(event: MouseEvent) { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
199 |
val line = y_to_line(event.getY) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
200 |
if (line >= 0 && line < text_area.getLineCount) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
201 |
text_area.setCaretPosition(text_area.getLineStartOffset(line)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
202 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
203 |
}) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
204 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
205 |
override def addNotify() { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
206 |
super.addNotify() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
207 |
ToolTipManager.sharedInstance.registerComponent(this) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
208 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
209 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
210 |
override def removeNotify() { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
211 |
ToolTipManager.sharedInstance.unregisterComponent(this) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
212 |
super.removeNotify |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
213 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
214 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
215 |
override def getToolTipText(event: MouseEvent): String = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
216 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
217 |
val line = y_to_line(event.getY()) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
218 |
if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>" |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
219 |
else "" |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
220 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
221 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
222 |
override def paintComponent(gfx: Graphics) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
223 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
224 |
super.paintComponent(gfx) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
225 |
val doc = model.current_document() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
226 |
val buffer = model.buffer |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
227 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
228 |
for (command <- doc.commands) { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
229 |
val line1 = buffer.getLineOfOffset(model.to_current(doc, command.start(doc))) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
230 |
val line2 = buffer.getLineOfOffset(model.to_current(doc, command.stop(doc))) + 1 |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
231 |
val y = line_to_y(line1) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
232 |
val height = HEIGHT * (line2 - line1) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
233 |
gfx.setColor(Document_View.choose_color(command, doc)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
234 |
gfx.fillRect(0, y, getWidth - 1, height) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
235 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
236 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
237 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
238 |
override def getPreferredSize = new Dimension(WIDTH, 0) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
239 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
240 |
private def line_to_y(line: Int): Int = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
241 |
(line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
242 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
243 |
private def y_to_line(y: Int): Int = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
244 |
(y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
245 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
246 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
247 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
248 |
private val selected_state_controller = new CaretListener |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
249 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
250 |
override def caretUpdate(e: CaretEvent) { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
251 |
val doc = model.current_document() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
252 |
doc.command_at(e.getDot) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
253 |
case Some(cmd) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
254 |
if (doc.token_start(cmd.tokens.first) <= e.getDot && |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
255 |
Isabelle.session.selected_state != cmd) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
256 |
Isabelle.session.selected_state = cmd // FIXME !? |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
257 |
case _ => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
258 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
259 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
260 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
261 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
262 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
263 |
/* activation */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
264 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
265 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
266 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
267 |
text_area.addCaretListener(selected_state_controller) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
268 |
text_area.addLeftOfScrollBar(overview) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
269 |
text_area.getPainter. |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
270 |
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
271 |
session.command_change += command_change_actor |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
272 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
273 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
274 |
def deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
275 |
{ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
276 |
session.command_change -= command_change_actor |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
277 |
command_change_actor !? Exit |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
278 |
text_area.getPainter.removeExtension(text_area_extension) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
279 |
text_area.removeLeftOfScrollBar(overview) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
280 |
text_area.removeCaretListener(selected_state_controller) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
281 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
282 |
} |