author | wenzelm |
Fri, 21 Sep 2012 17:41:29 +0200 | |
changeset 49513 | 796b3139f5a8 |
parent 49418 | c451856129cd |
parent 49494 | cbcccf2a0f6f |
child 49523 | dc0670364008 |
permissions | -rw-r--r-- |
49494
cbcccf2a0f6f
renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents:
49473
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/output_dockable.scala |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
3 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
4 |
Dockable window with result message output. |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
6 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
8 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
9 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
11 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
12 |
import scala.actors.Actor._ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
13 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
14 |
import scala.swing.{FlowPanel, Button, CheckBox} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
15 |
import scala.swing.event.ButtonClicked |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
16 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
17 |
import java.lang.System |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
18 |
import java.awt.BorderLayout |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
19 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
20 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
21 |
import org.gjt.sp.jedit.View |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
22 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
23 |
|
49494
cbcccf2a0f6f
renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents:
49473
diff
changeset
|
24 |
class Output_Dockable(view: View, position: String) extends Dockable(view, position) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
25 |
{ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
26 |
Swing_Thread.require() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
27 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
28 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
29 |
/* component state -- owned by Swing thread */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
30 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
31 |
private var zoom_factor = 100 |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
32 |
private var show_tracing = false |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
33 |
private var do_update = true |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
34 |
private var current_snapshot = Document.State.init.snapshot() |
49414 | 35 |
private var current_state = Command.empty.init_state |
49415 | 36 |
private var current_output: List[XML.Tree] = Nil |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
37 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
38 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
39 |
/* pretty text panel */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
40 |
|
49412 | 41 |
private val pretty_text_area = new Pretty_Text_Area(view) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
42 |
set_content(pretty_text_area) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
43 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
44 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
45 |
private def handle_resize() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
46 |
{ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
47 |
Swing_Thread.require() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
48 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
49 |
pretty_text_area.resize(Isabelle.font_family(), |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
50 |
scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
51 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
52 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
53 |
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
54 |
{ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
55 |
Swing_Thread.require() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
56 |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
57 |
val (new_snapshot, new_state) = |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
58 |
Document_View(view.getTextArea) match { |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
59 |
case Some(doc_view) => |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
60 |
val snapshot = doc_view.model.snapshot() |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
61 |
if (follow && !snapshot.is_outdated) { |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
62 |
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
63 |
case Some(cmd) => |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
64 |
(snapshot, snapshot.state.command_state(snapshot.version, cmd)) |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
65 |
case None => |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
66 |
(Document.State.init.snapshot(), Command.empty.init_state) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
67 |
} |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
68 |
} |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
69 |
else (current_snapshot, current_state) |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
70 |
case None => (current_snapshot, current_state) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
71 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
72 |
|
49415 | 73 |
val new_output = |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
74 |
if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
49418 | 75 |
new_state.results.iterator.map(_._2) |
76 |
.filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable |
|
49415 | 77 |
else current_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
78 |
|
49415 | 79 |
if (new_output != current_output) |
49473 | 80 |
pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output)) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
81 |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
82 |
current_snapshot = new_snapshot |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
83 |
current_state = new_state |
49415 | 84 |
current_output = new_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
85 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
86 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
87 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
88 |
/* main actor */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
89 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
90 |
private val main_actor = actor { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
91 |
loop { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
92 |
react { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
93 |
case Session.Global_Settings => |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
94 |
Swing_Thread.later { handle_resize() } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
95 |
case changed: Session.Commands_Changed => |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
96 |
Swing_Thread.later { handle_update(do_update, Some(changed.commands)) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
97 |
case Session.Caret_Focus => |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
98 |
Swing_Thread.later { handle_update(do_update, None) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
99 |
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
100 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
101 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
102 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
103 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
104 |
override def init() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
105 |
{ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
106 |
Swing_Thread.require() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
107 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
108 |
Isabelle.session.global_settings += main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
109 |
Isabelle.session.commands_changed += main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
110 |
Isabelle.session.caret_focus += main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
111 |
handle_update(true, None) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
112 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
113 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
114 |
override def exit() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
115 |
{ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
116 |
Swing_Thread.require() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
117 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
118 |
Isabelle.session.global_settings -= main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
119 |
Isabelle.session.commands_changed -= main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
120 |
Isabelle.session.caret_focus -= main_actor |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
121 |
delay_resize.revoke() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
122 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
123 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
124 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
125 |
/* resize */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
126 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
127 |
private val delay_resize = |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
128 |
Swing_Thread.delay_first( |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
129 |
Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
130 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
131 |
addComponentListener(new ComponentAdapter { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
132 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
133 |
}) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
134 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
135 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
136 |
/* controls */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
137 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
138 |
private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
139 |
zoom.tooltip = "Zoom factor for basic font size" |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
140 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
141 |
private val tracing = new CheckBox("Tracing") { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
142 |
reactions += { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
143 |
case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
144 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
145 |
tracing.selected = show_tracing |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
146 |
tracing.tooltip = "Indicate output of tracing messages" |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
147 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
148 |
private val auto_update = new CheckBox("Auto update") { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
149 |
reactions += { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
150 |
case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
151 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
152 |
auto_update.selected = do_update |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
153 |
auto_update.tooltip = "Indicate automatic update following cursor movement" |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
154 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
155 |
private val update = new Button("Update") { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
156 |
reactions += { case ButtonClicked(_) => handle_update(true, None) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
157 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
158 |
update.tooltip = "Update display according to the command at cursor position" |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
159 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
160 |
private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
161 |
add(controls.peer, BorderLayout.NORTH) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
162 |
} |