--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 12:13:53 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 12:21:25 2013 +0200
@@ -106,8 +106,7 @@
/* controls */
private def clicked {
- sledgehammer.apply_query(
- List(provers.getText, timeout.text, subgoal.text, isar_proofs.selected.toString))
+ sledgehammer.apply_query(List(provers.getText, timeout.text, isar_proofs.selected.toString))
}
private val provers_label = new Label("Provers:") {
@@ -130,12 +129,6 @@
s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }
}
- private val subgoal = new TextField("1", 5) {
- tooltip = "Subgoal number"
- verifier = (s: String) =>
- s match { case Properties.Value.Int(x) => x > 0 case _ => false }
- }
-
private val isar_proofs = new CheckBox("Isar proofs") {
tooltip = "Specify whether Isar proofs should be output in addition to metis line"
selected = false
@@ -162,7 +155,7 @@
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(
- provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs,
+ provers_label, Component.wrap(provers), timeout, isar_proofs,
process_indicator.component, apply_query, cancel_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)
}