author | wenzelm |
Sat, 10 Sep 2011 20:22:22 +0200 | |
changeset 44866 | 0eb8284a64bd |
parent 44865 | 679f0d57e831 |
child 44867 | 79d3d74e7cbb |
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._ |
|
44609 | 13 |
import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, |
14 |
ScrollPane, TabbedPane, Component, Swing} |
|
39638 | 15 |
import scala.swing.event.{ButtonClicked, 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 |
44866 | 18 |
import java.awt.{BorderLayout, Graphics} |
19 |
import javax.swing.{JList, DefaultListCellRenderer} |
|
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) |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43606
diff
changeset
|
30 |
readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html")))) |
39591 | 31 |
|
44609 | 32 |
val status = new ListView(Nil: List[String]) |
33 |
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) |
|
34 |
status.selection.intervalMode = ListView.IntervalMode.Single |
|
35 |
||
39629 | 36 |
private val syslog = new TextArea(Isabelle.session.syslog()) |
39591 | 37 |
|
38 |
private val tabs = new TabbedPane { |
|
39 |
pages += new TabbedPane.Page("README", Component.wrap(readme)) |
|
44609 | 40 |
pages += new TabbedPane.Page("Theory Status", new ScrollPane(status)) |
41 |
pages += new TabbedPane.Page("System Log", new ScrollPane(syslog)) |
|
39638 | 42 |
|
43 |
selection.index = |
|
44 |
{ |
|
45 |
val index = Isabelle.Int_Property("session-panel.selection", 0) |
|
46 |
if (index >= pages.length) 0 else index |
|
47 |
} |
|
48 |
listenTo(selection) |
|
49 |
reactions += { |
|
50 |
case SelectionChanged(_) => |
|
51 |
Isabelle.Int_Property("session-panel.selection") = selection.index |
|
52 |
} |
|
39591 | 53 |
} |
54 |
||
55 |
set_content(tabs) |
|
39515 | 56 |
|
57 |
||
39593 | 58 |
/* controls */ |
59 |
||
39635 | 60 |
val session_phase = new Label(Isabelle.session.phase.toString) |
39697 | 61 |
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) |
62 |
session_phase.tooltip = "Prover status" |
|
39635 | 63 |
|
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
64 |
private val cancel = new Button("Cancel") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
65 |
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() } |
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
66 |
} |
44865 | 67 |
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
|
68 |
|
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
69 |
private val check = new Button("Check") { |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44776
diff
changeset
|
70 |
reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) } |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
71 |
} |
44865 | 72 |
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
73 |
|
39702 | 74 |
private val logic = Isabelle.logic_selector(Isabelle.Property("logic")) |
75 |
logic.listenTo(logic.selection) |
|
76 |
logic.reactions += { |
|
77 |
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name |
|
78 |
} |
|
79 |
||
44775
27930cf6f0f7
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents:
44734
diff
changeset
|
80 |
private val controls = |
44776
47e8c8daccae
added "check" button: adhoc change to full buffer perspective;
wenzelm
parents:
44775
diff
changeset
|
81 |
new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic) |
39593 | 82 |
add(controls.peer, BorderLayout.NORTH) |
83 |
||
84 |
||
44609 | 85 |
/* component state -- owned by Swing thread */ |
86 |
||
44866 | 87 |
private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty |
88 |
||
89 |
val node_renderer = new DefaultListCellRenderer |
|
90 |
{ |
|
91 |
override def paintComponent(gfx: Graphics) |
|
92 |
{ |
|
93 |
super.paintComponent(gfx) |
|
94 |
nodes_status.get(Document.Node.Name(getText, "", "")) match { |
|
95 |
case Some(st) if st.total > 0 => |
|
96 |
val w = getWidth |
|
97 |
val h = getHeight |
|
98 |
var end = w |
|
99 |
for { |
|
100 |
(n, color) <- List( |
|
101 |
(st.unprocessed, Isabelle_Markup.unprocessed1_color), |
|
102 |
(st.running, Isabelle_Markup.running1_color), |
|
103 |
(st.failed, Isabelle_Markup.error1_color)) } |
|
104 |
{ |
|
105 |
gfx.setColor(color) |
|
106 |
val v = (n * w / st.total) max (if (n > 0) 2 else 0) |
|
107 |
gfx.fillRect(end - v, 0, v, h) |
|
108 |
end -= v |
|
109 |
} |
|
110 |
case _ => |
|
111 |
} |
|
112 |
} |
|
113 |
} |
|
114 |
||
115 |
status.peer.setCellRenderer(node_renderer) |
|
44609 | 116 |
|
44615 | 117 |
private def handle_changed(changed_nodes: Set[Document.Node.Name]) |
44609 | 118 |
{ |
119 |
Swing_Thread.now { |
|
44613 | 120 |
// FIXME correlation to changed_nodes!? |
121 |
val state = Isabelle.session.current_state() |
|
44672 | 122 |
val version = state.recent_stable.version.get_finished |
44613 | 123 |
|
44672 | 124 |
var nodes_status1 = nodes_status |
125 |
for { |
|
126 |
name <- changed_nodes |
|
127 |
node <- version.nodes.get(name) |
|
128 |
val status = Isar_Document.node_status(state, version, node) |
|
44866 | 129 |
} nodes_status1 += (name -> status) |
44672 | 130 |
|
131 |
if (nodes_status != nodes_status1) { |
|
132 |
nodes_status = nodes_status1 |
|
44866 | 133 |
status.listData = |
134 |
Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList) |
|
135 |
.map(_.node) |
|
44609 | 136 |
} |
137 |
} |
|
138 |
} |
|
139 |
||
140 |
||
39515 | 141 |
/* main actor */ |
142 |
||
143 |
private val main_actor = actor { |
|
144 |
loop { |
|
145 |
react { |
|
39589 | 146 |
case result: Isabelle_Process.Result => |
39625 | 147 |
if (result.is_syslog) |
148 |
Swing_Thread.now { |
|
39629 | 149 |
val text = Isabelle.session.syslog() |
39626
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
150 |
if (text != syslog.text) { |
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
151 |
syslog.text = text |
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
152 |
} |
39625 | 153 |
} |
39589 | 154 |
|
39701 | 155 |
case phase: Session.Phase => |
39696 | 156 |
Swing_Thread.now { session_phase.text = " " + phase.toString + " " } |
39635 | 157 |
|
44609 | 158 |
case changed: Session.Commands_Changed => handle_changed(changed.nodes) |
159 |
||
39515 | 160 |
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) |
161 |
} |
|
162 |
} |
|
163 |
} |
|
164 |
||
39635 | 165 |
override def init() { |
44734
7313e2db3d39
more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents:
44672
diff
changeset
|
166 |
Isabelle.session.syslog_messages += main_actor |
39635 | 167 |
Isabelle.session.phase_changed += main_actor |
44609 | 168 |
Isabelle.session.commands_changed += main_actor |
39635 | 169 |
} |
170 |
||
171 |
override def exit() { |
|
44734
7313e2db3d39
more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents:
44672
diff
changeset
|
172 |
Isabelle.session.syslog_messages -= main_actor |
39635 | 173 |
Isabelle.session.phase_changed -= main_actor |
44609 | 174 |
Isabelle.session.commands_changed -= main_actor |
39635 | 175 |
} |
39515 | 176 |
} |