69 addComponentListener(new ComponentAdapter { |
69 addComponentListener(new ComponentAdapter { |
70 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
70 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
71 }) |
71 }) |
72 |
72 |
73 |
73 |
|
74 /* provers according to ML */ |
|
75 |
|
76 private def update_provers() |
|
77 { |
|
78 val new_provers = Sledgehammer_Params.get_provers(PIDE.session) |
|
79 if (new_provers != "" && provers.getText == "") { |
|
80 provers.setText(new_provers) |
|
81 if (provers.getCaret != null) |
|
82 provers.getCaret.setDot(0) |
|
83 } |
|
84 } |
|
85 |
|
86 private def query_provers() |
|
87 { |
|
88 PIDE.session.protocol_command("Sledgehammer.provers") |
|
89 } |
|
90 |
|
91 |
74 /* main actor */ |
92 /* main actor */ |
75 |
93 |
76 private val main_actor = actor { |
94 private val main_actor = actor { |
77 loop { |
95 loop { |
78 react { |
96 react { |
79 case _: Session.Global_Options => |
97 case _: Session.Global_Options => |
80 Swing_Thread.later { handle_resize() } |
98 Swing_Thread.later { handle_resize() } |
|
99 query_provers() |
|
100 case Session.Ready => query_provers() |
|
101 case Sledgehammer_Params.Provers => |
|
102 Swing_Thread.later { update_provers() } |
81 case bad => |
103 case bad => |
82 java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad) |
104 java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad) |
83 } |
105 } |
84 } |
106 } |
85 } |
107 } |
86 |
108 |
87 override def init() |
109 override def init() |
88 { |
110 { |
89 Swing_Thread.require() |
111 Swing_Thread.require() |
90 |
112 |
|
113 PIDE.session.phase_changed += main_actor |
91 PIDE.session.global_options += main_actor |
114 PIDE.session.global_options += main_actor |
|
115 Sledgehammer_Params.provers += main_actor |
|
116 if (PIDE.session.is_ready) query_provers() |
92 handle_resize() |
117 handle_resize() |
93 sledgehammer.activate() |
118 sledgehammer.activate() |
94 } |
119 } |
95 |
120 |
96 override def exit() |
121 override def exit() |
97 { |
122 { |
98 Swing_Thread.require() |
123 Swing_Thread.require() |
99 |
124 |
100 sledgehammer.deactivate() |
125 sledgehammer.deactivate() |
|
126 PIDE.session.phase_changed -= main_actor |
101 PIDE.session.global_options -= main_actor |
127 PIDE.session.global_options -= main_actor |
|
128 Sledgehammer_Params.provers -= main_actor |
102 delay_resize.revoke() |
129 delay_resize.revoke() |
103 } |
130 } |
104 |
131 |
105 |
132 |
106 /* controls */ |
133 /* controls */ |
118 { |
145 { |
119 if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked |
146 if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked |
120 super.processKeyEvent(evt) |
147 super.processKeyEvent(evt) |
121 } |
148 } |
122 setToolTipText(provers_label.tooltip) |
149 setToolTipText(provers_label.tooltip) |
123 setColumns(20) |
150 setColumns(30) |
124 } |
151 } |
125 |
152 |
126 private val timeout = new TextField("30.0", 5) { |
153 private val timeout = new TextField("30.0", 5) { |
127 tooltip = "Soft time limit for each automatic prover (seconds > 0)" |
154 tooltip = "Soft time limit for each automatic prover (seconds > 0)" |
128 verifier = (s: String) => |
155 verifier = (s: String) => |