equal
deleted
inserted
replaced
99 private val provers_label = new Label("Provers: ") { |
99 private val provers_label = new Label("Provers: ") { |
100 tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")" |
100 tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")" |
101 } |
101 } |
102 |
102 |
103 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
103 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
|
104 override def processKeyEvent(evt: KeyEvent) |
|
105 { |
|
106 if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked |
|
107 super.processKeyEvent(evt) |
|
108 } |
104 setToolTipText(provers_label.tooltip) |
109 setToolTipText(provers_label.tooltip) |
105 setColumns(20) |
110 setColumns(20) |
106 } |
111 } |
107 |
112 |
108 private val timeout = new TextField("30.0", 5) { |
113 private val timeout = new TextField("30.0", 5) { |