author | wenzelm |
Sat, 18 Jun 2011 12:58:41 +0200 | |
changeset 43434 | 2fd41645813d |
parent 43419 | 6ed49c52d463 |
child 43520 | cec9b95fa35d |
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 |
||
37067 | 17 |
import java.awt.BorderLayout |
37014 | 18 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
34748 | 19 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
import org.gjt.sp.jedit.View |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
|
34765 | 22 |
|
37067 | 23 |
class Output_Dockable(view: View, position: String) extends Dockable(view, position) |
34760 | 24 |
{ |
38223 | 25 |
Swing_Thread.require() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
26 |
|
39592 | 27 |
private val html_panel = |
37164 | 28 |
new HTML_Panel(Isabelle.system, 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
|
29 |
{ |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
30 |
override val handler: PartialFunction[HTML_Panel.Event, Unit] = { |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
31 |
case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" => |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
32 |
val text = elem.getFirstChild().getNodeValue() |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
33 |
|
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
34 |
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
|
35 |
case Some(doc_view) => |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
36 |
val cmd = current_command.get |
43419
6ed49c52d463
flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
wenzelm
parents:
43282
diff
changeset
|
37 |
val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get |
42978
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
38 |
val buffer = view.getBuffer |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
39 |
buffer.beginCompoundEdit() |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
40 |
buffer.remove(start_ofs, cmd.length) |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
41 |
buffer.insert(start_ofs, text) |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
42 |
buffer.endCompoundEdit() |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
43 |
case None => |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
44 |
} |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
45 |
} |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
46 |
} |
6b41a075251f
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents:
39592
diff
changeset
|
47 |
|
39518 | 48 |
set_content(html_panel) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
49 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
50 |
|
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
51 |
/* component state -- owned by Swing thread */ |
36988 | 52 |
|
37019 | 53 |
private var zoom_factor = 100 |
37131 | 54 |
private var show_tracing = false |
55 |
private var follow_caret = true |
|
56 |
private var current_command: Option[Command] = None |
|
37019 | 57 |
|
37131 | 58 |
|
59 |
private def handle_resize() |
|
60 |
{ |
|
37019 | 61 |
Swing_Thread.now { |
37164 | 62 |
html_panel.resize(Isabelle.font_family(), |
63 |
scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
|
37019 | 64 |
} |
37131 | 65 |
} |
36988 | 66 |
|
37849 | 67 |
private def handle_perspective(): Boolean = |
37131 | 68 |
Swing_Thread.now { |
69 |
Document_View(view.getTextArea) match { |
|
37849 | 70 |
case Some(doc_view) => |
71 |
val cmd = doc_view.selected_command() |
|
72 |
if (current_command == cmd) false |
|
73 |
else { current_command = cmd; true } |
|
74 |
case None => false |
|
37131 | 75 |
} |
76 |
} |
|
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
77 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
78 |
private def handle_update(restriction: Option[Set[Command]] = None) |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
79 |
{ |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
80 |
Swing_Thread.now { |
37849 | 81 |
if (follow_caret) handle_perspective() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
82 |
Document_View(view.getTextArea) match { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
83 |
case Some(doc_view) => |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
84 |
current_command match { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
85 |
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
43419
6ed49c52d463
flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
wenzelm
parents:
43282
diff
changeset
|
86 |
val snapshot = doc_view.update_snapshot() |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
87 |
val filtered_results = |
38872 | 88 |
snapshot.state(cmd).results.iterator.map(_._2) filter { |
39513
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
38872
diff
changeset
|
89 |
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
90 |
case _ => true |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
91 |
} |
38872 | 92 |
html_panel.render(filtered_results.toList) |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
93 |
case _ => |
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 |
case None => |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
96 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
97 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
98 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
99 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
100 |
|
37067 | 101 |
/* main actor */ |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
102 |
|
37067 | 103 |
private val main_actor = actor { |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
104 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
105 |
react { |
37019 | 106 |
case Session.Global_Settings => handle_resize() |
38360 | 107 |
case Session.Commands_Changed(changed) => handle_update(Some(changed)) |
37850 | 108 |
case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() |
37067 | 109 |
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
|
110 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
111 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
112 |
} |
34428
d69fd18f37f9
basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents:
34424
diff
changeset
|
113 |
|
37067 | 114 |
override def init() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
115 |
{ |
37849 | 116 |
Isabelle.session.global_settings += main_actor |
37129 | 117 |
Isabelle.session.commands_changed += main_actor |
37849 | 118 |
Isabelle.session.perspective += main_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
119 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
120 |
|
37067 | 121 |
override def exit() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
122 |
{ |
37849 | 123 |
Isabelle.session.global_settings -= main_actor |
37129 | 124 |
Isabelle.session.commands_changed -= main_actor |
37849 | 125 |
Isabelle.session.perspective -= main_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
126 |
} |
36988 | 127 |
|
128 |
||
37014 | 129 |
/* resize */ |
130 |
||
131 |
addComponentListener(new ComponentAdapter { |
|
37849 | 132 |
val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() } |
37014 | 133 |
override def componentResized(e: ComponentEvent) { delay() } |
134 |
}) |
|
135 |
||
136 |
||
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
137 |
/* controls */ |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
138 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
139 |
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
|
140 |
zoom.tooltip = "Zoom factor for basic font size" |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
141 |
|
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
142 |
private val tracing = new CheckBox("Tracing") { |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
143 |
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
144 |
} |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
145 |
tracing.selected = show_tracing |
37372 | 146 |
tracing.tooltip = "Indicate output of tracing messages" |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
147 |
|
37131 | 148 |
private val auto_update = new CheckBox("Auto update") { |
37130
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
149 |
reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
7f18edbbf618
more reactive message handling, notably for follow_caret mode;
wenzelm
parents:
37129
diff
changeset
|
150 |
} |
37131 | 151 |
auto_update.selected = follow_caret |
37372 | 152 |
auto_update.tooltip = "Indicate automatic update following cursor movement" |
36988 | 153 |
|
37131 | 154 |
private val update = new Button("Update") { |
37849 | 155 |
reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } |
37131 | 156 |
} |
37372 | 157 |
update.tooltip = "Update display according to the command at cursor position" |
37131 | 158 |
|
39592 | 159 |
private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
37039 | 160 |
add(controls.peer, BorderLayout.NORTH) |
161 |
||
36988 | 162 |
handle_update() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
163 |
} |