equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.actors.Actor._ |
12 import scala.actors.Actor._ |
13 import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component} |
13 import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, |
|
14 Component, Swing} |
14 import scala.swing.event.ButtonClicked |
15 import scala.swing.event.ButtonClicked |
15 |
16 |
16 import java.awt.BorderLayout |
17 import java.awt.BorderLayout |
17 |
18 |
18 import org.gjt.sp.jedit.View |
19 import org.gjt.sp.jedit.View |
36 set_content(tabs) |
37 set_content(tabs) |
37 |
38 |
38 |
39 |
39 /* controls */ |
40 /* controls */ |
40 |
41 |
|
42 val session_phase = new Label(Isabelle.session.phase.toString) |
|
43 session_phase.border = Swing.EtchedBorder(Swing.Lowered) |
|
44 session_phase.tooltip = "Prover process status" |
|
45 |
41 private val interrupt = new Button("Interrupt") { |
46 private val interrupt = new Button("Interrupt") { |
42 reactions += { case ButtonClicked(_) => Isabelle.session.interrupt } |
47 reactions += { case ButtonClicked(_) => Isabelle.session.interrupt } |
43 } |
48 } |
44 interrupt.tooltip = "Broadcast interrupt to all prover tasks" |
49 interrupt.tooltip = "Broadcast interrupt to all prover tasks" |
45 |
50 |
46 private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt) |
51 private val controls = |
|
52 new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt) |
47 add(controls.peer, BorderLayout.NORTH) |
53 add(controls.peer, BorderLayout.NORTH) |
48 |
54 |
49 |
55 |
50 /* main actor */ |
56 /* main actor */ |
51 |
57 |
59 if (text != syslog.text) { |
65 if (text != syslog.text) { |
60 syslog.text = text |
66 syslog.text = text |
61 } |
67 } |
62 } |
68 } |
63 |
69 |
|
70 case (_, phase: Session.Phase) => |
|
71 Swing_Thread.now { session_phase.text = phase.toString } |
|
72 |
64 case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) |
73 case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) |
65 } |
74 } |
66 } |
75 } |
67 } |
76 } |
68 |
77 |
69 override def init() { Isabelle.session.raw_messages += main_actor } |
78 override def init() { |
70 override def exit() { Isabelle.session.raw_messages -= main_actor } |
79 Isabelle.session.raw_messages += main_actor |
|
80 Isabelle.session.phase_changed += main_actor |
|
81 } |
|
82 |
|
83 override def exit() { |
|
84 Isabelle.session.raw_messages -= main_actor |
|
85 Isabelle.session.phase_changed -= main_actor |
|
86 } |
71 } |
87 } |