|
1 /* Title: Tools/jEdit/src/output1_dockable.scala |
|
2 Author: Makarius |
|
3 |
|
4 Dockable window with result message output. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.actors.Actor._ |
|
13 |
|
14 import scala.swing.{FlowPanel, Button, CheckBox} |
|
15 import scala.swing.event.ButtonClicked |
|
16 |
|
17 import java.lang.System |
|
18 import java.awt.BorderLayout |
|
19 import java.awt.event.{ComponentEvent, ComponentAdapter} |
|
20 |
|
21 import org.gjt.sp.jedit.View |
|
22 |
|
23 |
|
24 class Output1_Dockable(view: View, position: String) extends Dockable(view, position) |
|
25 { |
|
26 Swing_Thread.require() |
|
27 |
|
28 |
|
29 /* component state -- owned by Swing thread */ |
|
30 |
|
31 private var zoom_factor = 100 |
|
32 private var show_tracing = false |
|
33 private var do_update = true |
|
34 private var current_state = Command.empty.init_state |
|
35 private var current_body: XML.Body = Nil |
|
36 |
|
37 |
|
38 /* HTML panel */ |
|
39 |
|
40 private val html_panel = |
|
41 new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) |
|
42 { |
|
43 override val handler: PartialFunction[HTML_Panel.Event, Unit] = |
|
44 { |
|
45 case HTML_Panel.Mouse_Click(elem, event) |
|
46 if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined => |
|
47 val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get |
|
48 Document_View(view.getTextArea) match { |
|
49 case Some(doc_view) => |
|
50 doc_view.rich_text_area.robust_body() { |
|
51 val cmd = current_state.command |
|
52 val model = doc_view.model |
|
53 val buffer = model.buffer |
|
54 val snapshot = model.snapshot() |
|
55 snapshot.node.command_start(cmd) match { |
|
56 case Some(start) if !snapshot.is_outdated => |
|
57 val text = Pretty.string_of(sendback) |
|
58 try { |
|
59 buffer.beginCompoundEdit() |
|
60 buffer.remove(start, cmd.proper_range.length) |
|
61 buffer.insert(start, text) |
|
62 } |
|
63 finally { buffer.endCompoundEdit() } |
|
64 case _ => |
|
65 } |
|
66 } |
|
67 case None => |
|
68 } |
|
69 } |
|
70 } |
|
71 |
|
72 set_content(html_panel) |
|
73 |
|
74 |
|
75 private def handle_resize() |
|
76 { |
|
77 Swing_Thread.require() |
|
78 |
|
79 html_panel.resize(Isabelle.font_family(), |
|
80 scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
|
81 } |
|
82 |
|
83 private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) |
|
84 { |
|
85 Swing_Thread.require() |
|
86 |
|
87 val new_state = |
|
88 if (follow) { |
|
89 Document_View(view.getTextArea) match { |
|
90 case Some(doc_view) => |
|
91 val snapshot = doc_view.model.snapshot() |
|
92 snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
|
93 case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) |
|
94 case None => Command.empty.init_state |
|
95 } |
|
96 case None => Command.empty.init_state |
|
97 } |
|
98 } |
|
99 else current_state |
|
100 |
|
101 val new_body = |
|
102 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
|
103 new_state.results.iterator.map(_._2) |
|
104 .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable |
|
105 else current_body |
|
106 |
|
107 if (new_body != current_body) html_panel.render(new_body) |
|
108 |
|
109 current_state = new_state |
|
110 current_body = new_body |
|
111 } |
|
112 |
|
113 |
|
114 /* main actor */ |
|
115 |
|
116 private val main_actor = actor { |
|
117 loop { |
|
118 react { |
|
119 case Session.Global_Settings => |
|
120 Swing_Thread.later { handle_resize() } |
|
121 case changed: Session.Commands_Changed => |
|
122 Swing_Thread.later { handle_update(do_update, Some(changed.commands)) } |
|
123 case Session.Caret_Focus => |
|
124 Swing_Thread.later { handle_update(do_update, None) } |
|
125 case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
|
126 } |
|
127 } |
|
128 } |
|
129 |
|
130 override def init() |
|
131 { |
|
132 Swing_Thread.require() |
|
133 |
|
134 Isabelle.session.global_settings += main_actor |
|
135 Isabelle.session.commands_changed += main_actor |
|
136 Isabelle.session.caret_focus += main_actor |
|
137 handle_update(true, None) |
|
138 } |
|
139 |
|
140 override def exit() |
|
141 { |
|
142 Swing_Thread.require() |
|
143 |
|
144 Isabelle.session.global_settings -= main_actor |
|
145 Isabelle.session.commands_changed -= main_actor |
|
146 Isabelle.session.caret_focus -= main_actor |
|
147 delay_resize.revoke() |
|
148 } |
|
149 |
|
150 |
|
151 /* resize */ |
|
152 |
|
153 private val delay_resize = |
|
154 Swing_Thread.delay_first( |
|
155 Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } |
|
156 |
|
157 addComponentListener(new ComponentAdapter { |
|
158 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
159 }) |
|
160 |
|
161 |
|
162 /* controls */ |
|
163 |
|
164 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
|
165 zoom.tooltip = "Zoom factor for basic font size" |
|
166 |
|
167 private val tracing = new CheckBox("Tracing") { |
|
168 reactions += { |
|
169 case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) } |
|
170 } |
|
171 tracing.selected = show_tracing |
|
172 tracing.tooltip = "Indicate output of tracing messages" |
|
173 |
|
174 private val auto_update = new CheckBox("Auto update") { |
|
175 reactions += { |
|
176 case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } |
|
177 } |
|
178 auto_update.selected = do_update |
|
179 auto_update.tooltip = "Indicate automatic update following cursor movement" |
|
180 |
|
181 private val update = new Button("Update") { |
|
182 reactions += { case ButtonClicked(_) => handle_update(true, None) } |
|
183 } |
|
184 update.tooltip = "Update display according to the command at cursor position" |
|
185 |
|
186 private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
|
187 add(controls.peer, BorderLayout.NORTH) |
|
188 } |