author | wenzelm |
Sun, 26 Feb 2012 17:44:09 +0100 | |
changeset 46681 | c083a3f621c0 |
parent 45709 | 87017fcbad83 |
child 46688 | 134982ee4ecb |
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} |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
19 |
import javax.swing.{JList, DefaultListCellRenderer, 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 |
||
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43606
diff
changeset
|
29 |
private val readme = new HTML_Panel("SansSerif", 14) |
45099 | 30 |
private val readme_path = Path.explode("$JEDIT_HOME/README.html") |
45100 | 31 |
readme.render_document( |
32 |
Isabelle_System.platform_file_url(readme_path), |
|
33 |
Isabelle_System.try_read(List(readme_path))) |
|
39591 | 34 |
|
44991 | 35 |
val status = new ListView(Nil: List[Document.Node.Name]) { |
36 |
listenTo(mouse.clicks) |
|
37 |
reactions += { |
|
38 |
case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
|
39 |
val index = peer.locationToIndex(point) |
|
40 |
if (index >= 0) jEdit.openFile(view, listData(index).node) |
|
41 |
} |
|
42 |
} |
|
44609 | 43 |
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
44 |
status.selection.intervalMode = ListView.IntervalMode.Single |
|
45 |
||
39629 | 46 |
private val syslog = new TextArea(Isabelle.session.syslog()) |
39591 | 47 |
|
48 |
private val tabs = new TabbedPane { |
|
49 |
pages += new TabbedPane.Page("README", Component.wrap(readme)) |
|
44609 | 50 |
pages += new TabbedPane.Page("Theory Status", new ScrollPane(status)) |
51 |
pages += new TabbedPane.Page("System Log", new ScrollPane(syslog)) |
|
39638 | 52 |
|
53 |
selection.index = |
|
54 |
{ |
|
55 |
val index = Isabelle.Int_Property("session-panel.selection", 0) |
|
56 |
if (index >= pages.length) 0 else index |
|
57 |
} |
|
58 |
listenTo(selection) |
|
59 |
reactions += { |
|
60 |
case SelectionChanged(_) => |
|
61 |
Isabelle.Int_Property("session-panel.selection") = selection.index |
|
62 |
} |
|
39591 | 63 |
} |
64 |
||
65 |
set_content(tabs) |
|
39515 | 66 |
|
67 |
||
39593 | 68 |
/* controls */ |
69 |
||
39635 | 70 |
val session_phase = new Label(Isabelle.session.phase.toString) |
39697 | 71 |
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) |
72 |
session_phase.tooltip = "Prover status" |
|
39635 | 73 |
|
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
74 |
private val cancel = new Button("Cancel") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
75 |
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() } |
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
76 |
} |
44865 | 77 |
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
|
78 |
|
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
79 |
private val check = new Button("Check") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
80 |
reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) } |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
81 |
} |
44865 | 82 |
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
83 |
|
39702 | 84 |
private val logic = Isabelle.logic_selector(Isabelle.Property("logic")) |
85 |
logic.listenTo(logic.selection) |
|
86 |
logic.reactions += { |
|
87 |
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name |
|
88 |
} |
|
89 |
||
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
90 |
private val controls = |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
91 |
new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic) |
39593 | 92 |
add(controls.peer, BorderLayout.NORTH) |
93 |
||
94 |
||
44609 | 95 |
/* component state -- owned by Swing thread */ |
96 |
||
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
97 |
private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty |
44866 | 98 |
|
44990 | 99 |
private object Node_Renderer_Component extends Label |
44866 | 100 |
{ |
44990 | 101 |
opaque = false |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
102 |
xAlignment = Alignment.Leading |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
103 |
border = BorderFactory.createEmptyBorder(2, 2, 2, 2) |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
104 |
|
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
105 |
var node_name = Document.Node.Name.empty |
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
106 |
override def paintComponent(gfx: Graphics2D) |
44866 | 107 |
{ |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
108 |
nodes_status.get(node_name) match { |
44866 | 109 |
case Some(st) if st.total > 0 => |
44958 | 110 |
val size = peer.getSize() |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
111 |
val insets = border.getBorderInsets(this.peer) |
44958 | 112 |
val w = size.width - insets.left - insets.right |
113 |
val h = size.height - insets.top - insets.bottom |
|
114 |
var end = size.width - insets.right |
|
44866 | 115 |
for { |
116 |
(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
|
117 |
(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
|
118 |
(st.running, Isabelle_Rendering.running_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
|
119 |
(st.failed, Isabelle_Rendering.error_color)) } |
44866 | 120 |
{ |
121 |
gfx.setColor(color) |
|
122 |
val v = (n * w / st.total) max (if (n > 0) 2 else 0) |
|
44958 | 123 |
gfx.fillRect(end - v, insets.top, v, h) |
44866 | 124 |
end -= v |
125 |
} |
|
126 |
case _ => |
|
127 |
} |
|
44867 | 128 |
super.paintComponent(gfx) |
44866 | 129 |
} |
130 |
} |
|
131 |
||
44990 | 132 |
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
|
133 |
{ |
44990 | 134 |
def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, |
135 |
name: Document.Node.Name, index: Int): Component = |
|
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
136 |
{ |
44990 | 137 |
val component = Node_Renderer_Component |
44957
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
138 |
component.node_name = name |
44989
5450ab3c677e
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents:
44981
diff
changeset
|
139 |
component.text = name.theory |
44990 | 140 |
component |
44957
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 |
} |
098dd95349e7
more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents:
44867
diff
changeset
|
143 |
status.renderer = new Node_Renderer |
44609 | 144 |
|
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
145 |
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) |
44609 | 146 |
{ |
147 |
Swing_Thread.now { |
|
44960 | 148 |
val snapshot = Isabelle.session.snapshot() |
46681 | 149 |
val names = restriction getOrElse snapshot.version.nodes.keySet |
44613 | 150 |
|
46681 | 151 |
val nodes_status1 = |
152 |
(nodes_status /: names)((status, name) => { |
|
153 |
val node = snapshot.version.nodes(name) |
|
154 |
status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) |
|
155 |
}) |
|
44672 | 156 |
|
157 |
if (nodes_status != nodes_status1) { |
|
158 |
nodes_status = nodes_status1 |
|
44866 | 159 |
status.listData = |
44960 | 160 |
snapshot.version.topological_order.filter( |
161 |
(name: Document.Node.Name) => nodes_status.isDefinedAt(name)) |
|
44609 | 162 |
} |
163 |
} |
|
164 |
} |
|
165 |
||
166 |
||
39515 | 167 |
/* main actor */ |
168 |
||
169 |
private val main_actor = actor { |
|
170 |
loop { |
|
171 |
react { |
|
39589 | 172 |
case result: Isabelle_Process.Result => |
39625 | 173 |
if (result.is_syslog) |
174 |
Swing_Thread.now { |
|
39629 | 175 |
val text = Isabelle.session.syslog() |
39626
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
176 |
if (text != syslog.text) { |
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
177 |
syslog.text = text |
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
178 |
} |
39625 | 179 |
} |
39589 | 180 |
|
39701 | 181 |
case phase: Session.Phase => |
39696 | 182 |
Swing_Thread.now { session_phase.text = " " + phase.toString + " " } |
39635 | 183 |
|
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
184 |
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) |
44609 | 185 |
|
39515 | 186 |
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) |
187 |
} |
|
188 |
} |
|
189 |
} |
|
190 |
||
39635 | 191 |
override def init() { |
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 |
44609 | 194 |
Isabelle.session.commands_changed += main_actor |
39635 | 195 |
} |
196 |
||
197 |
override def exit() { |
|
44734
7313e2db3d39
more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents:
44672
diff
changeset
|
198 |
Isabelle.session.syslog_messages -= main_actor |
39635 | 199 |
Isabelle.session.phase_changed -= main_actor |
44609 | 200 |
Isabelle.session.commands_changed -= main_actor |
39635 | 201 |
} |
45011
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
202 |
|
436ea69d5d37
more careful treatment of initial update, similar to output panel;
wenzelm
parents:
44991
diff
changeset
|
203 |
handle_update() |
39515 | 204 |
} |