author | wenzelm |
Tue, 29 May 2012 20:38:40 +0200 | |
changeset 48018 | b941dd7df92a |
parent 48014 | 63021e59cbf0 |
child 48021 | d899be1cfe6d |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
39736
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/session_dockable.scala |
39515 | 2 |
Author: Makarius |
3 |
||
4 |
Dockable window for prover session management. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import scala.actors.Actor._ |
|
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
13 |
import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, |
44609 | 14 |
ScrollPane, TabbedPane, Component, Swing} |
44991 | 15 |
import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged} |
39593 | 16 |
|
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43282
diff
changeset
|
17 |
import java.lang.System |
44980
ad5883642a83
more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);
wenzelm
parents:
44960
diff
changeset
|
18 |
import java.awt.{BorderLayout, Graphics2D, Insets} |
47588 | 19 |
import javax.swing.{JList, BorderFactory} |
39697 | 20 |
import javax.swing.border.{BevelBorder, SoftBevelBorder} |
39515 | 21 |
|
44865 | 22 |
import org.gjt.sp.jedit.{View, jEdit} |
39515 | 23 |
|
24 |
||
25 |
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String) |
|
26 |
{ |
|
39591 | 27 |
/* main tabs */ |
28 |
||
44991 | 29 |
val status = new ListView(Nil: List[Document.Node.Name]) { |
30 |
listenTo(mouse.clicks) |
|
31 |
reactions += { |
|
32 |
case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
|
33 |
val index = peer.locationToIndex(point) |
|
34 |
if (index >= 0) jEdit.openFile(view, listData(index).node) |
|
35 |
} |
|
36 |
} |
|
44609 | 37 |
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
38 |
status.selection.intervalMode = ListView.IntervalMode.Single |
|
39 |
||
46771
06a9b24c4a36
explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents:
46739
diff
changeset
|
40 |
private val syslog = new TextArea(Isabelle.session.current_syslog()) |
39591 | 41 |
|
42 |
private val tabs = new TabbedPane { |
|
44609 | 43 |
pages += new TabbedPane.Page("Theory Status", new ScrollPane(status)) |
44 |
pages += new TabbedPane.Page("System Log", new ScrollPane(syslog)) |
|
39638 | 45 |
|
46 |
selection.index = |
|
47 |
{ |
|
48 |
val index = Isabelle.Int_Property("session-panel.selection", 0) |
|
49 |
if (index >= pages.length) 0 else index |
|
50 |
} |
|
51 |
listenTo(selection) |
|
52 |
reactions += { |
|
53 |
case SelectionChanged(_) => |
|
54 |
Isabelle.Int_Property("session-panel.selection") = selection.index |
|
55 |
} |
|
39591 | 56 |
} |
57 |
||
58 |
set_content(tabs) |
|
39515 | 59 |
|
60 |
||
39593 | 61 |
/* controls */ |
62 |
||
39635 | 63 |
val session_phase = new Label(Isabelle.session.phase.toString) |
39697 | 64 |
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) |
65 |
session_phase.tooltip = "Prover status" |
|
39635 | 66 |
|
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
67 |
private def handle_phase(phase: Session.Phase) |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
68 |
{ |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
69 |
Swing_Thread.later { session_phase.text = " " + phase.toString + " " } |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
70 |
} |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
71 |
|
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
72 |
private val cancel = new Button("Cancel") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
73 |
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() } |
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
74 |
} |
44865 | 75 |
cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label") |
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
76 |
|
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
77 |
private val check = new Button("Check") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
78 |
reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) } |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
79 |
} |
44865 | 80 |
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
81 |
|
39702 | 82 |
private val logic = Isabelle.logic_selector(Isabelle.Property("logic")) |
83 |
logic.listenTo(logic.selection) |
|
84 |
logic.reactions += { |
|
85 |
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name |
|
86 |
} |
|
87 |
||
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
88 |
private val controls = |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
89 |
new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic) |
39593 | 90 |
add(controls.peer, BorderLayout.NORTH) |
91 |
||
92 |
||
44609 | 93 |
/* component state -- owned by Swing thread */ |
94 |
||
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
95 |
private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty |
44866 | 96 |
|
44990 | 97 |
private object Node_Renderer_Component extends Label |
44866 | 98 |
{ |
44990 | 99 |
opaque = false |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
100 |
xAlignment = Alignment.Leading |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
101 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
102 |
|
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
103 |
var node_name = Document.Node.Name.empty |
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
104 |
override def paintComponent(gfx: Graphics2D) |
44866 | 105 |
{ |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
106 |
nodes_status.get(node_name) match { |
44866 | 107 |
case Some(st) if st.total > 0 => |
44958 | 108 |
val size = peer.getSize() |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
109 |
val insets = border.getBorderInsets(this.peer) |
44958 | 110 |
val w = size.width - insets.left - insets.right |
111 |
val h = size.height - insets.top - insets.bottom |
|
112 |
var end = size.width - insets.right |
|
44866 | 113 |
for { |
114 |
(n, color) <- List( |
|
45665
129db1416717
renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents:
45100
diff
changeset
|
115 |
(st.unprocessed, Isabelle_Rendering.unprocessed1_color), |
129db1416717
renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents:
45100
diff
changeset
|
116 |
(st.running, Isabelle_Rendering.running_color), |
46688 | 117 |
(st.warned, Isabelle_Rendering.warning_color), |
45665
129db1416717
renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents:
45100
diff
changeset
|
118 |
(st.failed, Isabelle_Rendering.error_color)) } |
44866 | 119 |
{ |
120 |
gfx.setColor(color) |
|
121 |
val v = (n * w / st.total) max (if (n > 0) 2 else 0) |
|
44958 | 122 |
gfx.fillRect(end - v, insets.top, v, h) |
44866 | 123 |
end -= v |
124 |
} |
|
125 |
case _ => |
|
126 |
} |
|
44867 | 127 |
super.paintComponent(gfx) |
44866 | 128 |
} |
129 |
} |
|
130 |
||
44990 | 131 |
private class Node_Renderer extends ListView.Renderer[Document.Node.Name] |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
132 |
{ |
44990 | 133 |
def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, |
134 |
name: Document.Node.Name, index: Int): Component = |
|
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
135 |
{ |
44990 | 136 |
val component = Node_Renderer_Component |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
137 |
component.node_name = name |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
138 |
component.text = name.theory |
44990 | 139 |
component |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
140 |
} |
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
141 |
} |
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
142 |
status.renderer = new Node_Renderer |
44609 | 143 |
|
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
144 |
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) |
44609 | 145 |
{ |
146 |
Swing_Thread.now { |
|
44960 | 147 |
val snapshot = Isabelle.session.snapshot() |
44613 | 148 |
|
46723 | 149 |
val iterator = |
150 |
restriction match { |
|
151 |
case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) |
|
152 |
case None => snapshot.version.nodes.entries |
|
153 |
} |
|
46681 | 154 |
val nodes_status1 = |
46723 | 155 |
(nodes_status /: iterator)({ case (status, (name, node)) => |
46739
6024353549ca
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents:
46723
diff
changeset
|
156 |
if (Isabelle.thy_load.is_loaded(name.theory)) status |
6024353549ca
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents:
46723
diff
changeset
|
157 |
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) |
44672 | 158 |
|
159 |
if (nodes_status != nodes_status1) { |
|
160 |
nodes_status = nodes_status1 |
|
44866 | 161 |
status.listData = |
46723 | 162 |
snapshot.version.nodes.topological_order.filter( |
44960 | 163 |
(name: Document.Node.Name) => nodes_status.isDefinedAt(name)) |
44609 | 164 |
} |
165 |
} |
|
166 |
} |
|
167 |
||
168 |
||
39515 | 169 |
/* main actor */ |
170 |
||
171 |
private val main_actor = actor { |
|
172 |
loop { |
|
173 |
react { |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46771
diff
changeset
|
174 |
case output: Isabelle_Process.Output => |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46771
diff
changeset
|
175 |
if (output.is_syslog) |
46918
1752164d916b
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents:
46772
diff
changeset
|
176 |
Swing_Thread.later { |
46771
06a9b24c4a36
explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents:
46739
diff
changeset
|
177 |
val text = Isabelle.session.current_syslog() |
06a9b24c4a36
explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents:
46739
diff
changeset
|
178 |
if (text != syslog.text) syslog.text = text |
39625 | 179 |
} |
39589 | 180 |
|
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
181 |
case phase: Session.Phase => handle_phase(phase) |
39635 | 182 |
|
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
183 |
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) |
44609 | 184 |
|
39515 | 185 |
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) |
186 |
} |
|
187 |
} |
|
188 |
} |
|
189 |
||
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
190 |
override def init() |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
191 |
{ |
44734
7313e2db3d39
more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents:
44672
diff
changeset
|
192 |
Isabelle.session.syslog_messages += main_actor |
39635 | 193 |
Isabelle.session.phase_changed += main_actor |
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
194 |
handle_phase(Isabelle.session.phase) |
44609 | 195 |
Isabelle.session.commands_changed += main_actor |
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
196 |
handle_update() |
39635 | 197 |
} |
198 |
||
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
199 |
override def exit() |
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
200 |
{ |
44734
7313e2db3d39
more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents:
44672
diff
changeset
|
201 |
Isabelle.session.syslog_messages -= main_actor |
39635 | 202 |
Isabelle.session.phase_changed -= main_actor |
44609 | 203 |
Isabelle.session.commands_changed -= main_actor |
39635 | 204 |
} |
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
205 |
|
48018
b941dd7df92a
make double sure that GUI components are up-to-date after init;
wenzelm
parents:
48014
diff
changeset
|
206 |
handle_phase(Isabelle.session.phase) |
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
207 |
handle_update() |
39515 | 208 |
} |