author | wenzelm |
Tue, 11 Sep 2012 19:19:39 +0200 | |
changeset 49288 | 2c9272cb4568 |
parent 49195 | 9d10bd85c1be |
child 49359 | c1262d7389fb |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
42978
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/output_dockable.scala |
36760 | 2 |
Author: Makarius |
3 |
||
4 |
Dockable window with result message output. |
|
5 |
*/ |
|
34408 | 6 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
34760 | 9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
12 |
import scala.actors.Actor._ |
34760 | 13 |
|
37017
cf6625012282
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
wenzelm
parents:
37014
diff
changeset
|
14 |
import scala.swing.{FlowPanel, Button, CheckBox} |
36988 | 15 |
import scala.swing.event.ButtonClicked |
16 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43419
diff
changeset
|
17 |
import java.lang.System |
37067 | 18 |
import java.awt.BorderLayout |
37014 | 19 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
34748 | 20 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
import org.gjt.sp.jedit.View |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
|
34765 | 23 |
|
37067 | 24 |
class Output_Dockable(view: View, position: String) extends Dockable(view, position) |
34760 | 25 |
{ |
38223 | 26 |
Swing_Thread.require() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
27 |
|
39592 | 28 |
private val html_panel = |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
29 |
new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) |
42978
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
30 |
{ |
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
31 |
override val handler: PartialFunction[HTML_Panel.Event, Unit] = |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
32 |
{ |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
33 |
case HTML_Panel.Mouse_Click(elem, event) |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
34 |
if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined => |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
35 |
val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get |
42978
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
36 |
Document_View(view.getTextArea) match { |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
37 |
case Some(doc_view) => |
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
38 |
doc_view.robust_body() { |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
39 |
current_command match { |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
40 |
case Some(cmd) => |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
41 |
val model = doc_view.model |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
42 |
val buffer = model.buffer |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
43 |
val snapshot = model.snapshot() |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
44 |
snapshot.node.command_start(cmd) match { |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
45 |
case Some(start) if !snapshot.is_outdated => |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
46 |
val text = Pretty.string_of(sendback) |
47587 | 47 |
try { |
48 |
buffer.beginCompoundEdit() |
|
49 |
buffer.remove(start, cmd.proper_range.length) |
|
50 |
buffer.insert(start, text) |
|
51 |
} |
|
52 |
finally { buffer.endCompoundEdit() } |
|
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
53 |
case _ => |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
54 |
} |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
55 |
case None => |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
56 |
} |
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
57 |
} |
42978
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
58 |
case None => |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
59 |
} |
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
47027
diff
changeset
|
60 |
} |
42978
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
61 |
} |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
62 |
|
39518 | 63 |
set_content(html_panel) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
64 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
65 |
|
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
66 |
/* component state -- owned by Swing thread */ |
36988 | 67 |
|
37019 | 68 |
private var zoom_factor = 100 |
37131 | 69 |
private var show_tracing = false |
70 |
private var follow_caret = true |
|
71 |
private var current_command: Option[Command] = None |
|
37019 | 72 |
|
37131 | 73 |
|
74 |
private def handle_resize() |
|
75 |
{ |
|
37019 | 76 |
Swing_Thread.now { |
37164 | 77 |
html_panel.resize(Isabelle.font_family(), |
78 |
scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
|
37019 | 79 |
} |
37131 | 80 |
} |
36988 | 81 |
|
37849 | 82 |
private def handle_perspective(): Boolean = |
37131 | 83 |
Swing_Thread.now { |
84 |
Document_View(view.getTextArea) match { |
|
37849 | 85 |
case Some(doc_view) => |
86 |
val cmd = doc_view.selected_command() |
|
87 |
if (current_command == cmd) false |
|
88 |
else { current_command = cmd; true } |
|
89 |
case None => false |
|
37131 | 90 |
} |
91 |
} |
|
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
92 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
93 |
private def handle_update(restriction: Option[Set[Command]] = None) |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
94 |
{ |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
95 |
Swing_Thread.now { |
37849 | 96 |
if (follow_caret) handle_perspective() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
97 |
Document_View(view.getTextArea) match { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
98 |
case Some(doc_view) => |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
99 |
current_command match { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
100 |
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
47027
fc3bb6c02a3c
explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents:
46740
diff
changeset
|
101 |
val snapshot = doc_view.model.snapshot() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
102 |
val filtered_results = |
46208 | 103 |
snapshot.state.command_state(snapshot.version, cmd).results.iterator |
104 |
.map(_._2).filter( |
|
105 |
{ // FIXME not scalable |
|
106 |
case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
|
107 |
case _ => true |
|
108 |
}).toList |
|
109 |
html_panel.render(filtered_results) |
|
49071
c1ca931b3647
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
wenzelm
parents:
48026
diff
changeset
|
110 |
case _ => html_panel.render(Nil) |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
111 |
} |
49071
c1ca931b3647
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
wenzelm
parents:
48026
diff
changeset
|
112 |
case None => html_panel.render(Nil) |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
113 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
114 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
115 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
116 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
117 |
|
37067 | 118 |
/* main actor */ |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
119 |
|
37067 | 120 |
private val main_actor = actor { |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
121 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
122 |
react { |
37019 | 123 |
case Session.Global_Settings => handle_resize() |
44608 | 124 |
case changed: Session.Commands_Changed => handle_update(Some(changed.commands)) |
44805 | 125 |
case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update() |
37067 | 126 |
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
127 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
128 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
129 |
} |
34428
d69fd18f37f9
basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents:
34424
diff
changeset
|
130 |
|
37067 | 131 |
override def init() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
132 |
{ |
37849 | 133 |
Isabelle.session.global_settings += main_actor |
37129 | 134 |
Isabelle.session.commands_changed += main_actor |
44805 | 135 |
Isabelle.session.caret_focus += main_actor |
48026 | 136 |
handle_update() |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
137 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
138 |
|
37067 | 139 |
override def exit() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
140 |
{ |
37849 | 141 |
Isabelle.session.global_settings -= main_actor |
37129 | 142 |
Isabelle.session.commands_changed -= main_actor |
44805 | 143 |
Isabelle.session.caret_focus -= main_actor |
49195 | 144 |
delay_resize.revoke() |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
145 |
} |
36988 | 146 |
|
147 |
||
37014 | 148 |
/* resize */ |
149 |
||
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46571
diff
changeset
|
150 |
private val delay_resize = |
49288 | 151 |
Swing_Thread.delay_first( |
152 |
Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } |
|
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46571
diff
changeset
|
153 |
|
37014 | 154 |
addComponentListener(new ComponentAdapter { |
49195 | 155 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
37014 | 156 |
}) |
157 |
||
158 |
||
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
159 |
/* controls */ |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
160 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
161 |
private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
162 |
zoom.tooltip = "Zoom factor for basic font size" |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
163 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
164 |
private val tracing = new CheckBox("Tracing") { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
165 |
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
166 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
167 |
tracing.selected = show_tracing |
37372 | 168 |
tracing.tooltip = "Indicate output of tracing messages" |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
169 |
|
37131 | 170 |
private val auto_update = new CheckBox("Auto update") { |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
171 |
reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
172 |
} |
37131 | 173 |
auto_update.selected = follow_caret |
37372 | 174 |
auto_update.tooltip = "Indicate automatic update following cursor movement" |
36988 | 175 |
|
37131 | 176 |
private val update = new Button("Update") { |
37849 | 177 |
reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } |
37131 | 178 |
} |
37372 | 179 |
update.tooltip = "Update display according to the command at cursor position" |
37131 | 180 |
|
39592 | 181 |
private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
37039 | 182 |
add(controls.peer, BorderLayout.NORTH) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
183 |
} |