equal
deleted
inserted
replaced
135 sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString)) |
135 sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString)) |
136 } |
136 } |
137 |
137 |
138 private val provers_label = new Label("Provers:") { |
138 private val provers_label = new Label("Provers:") { |
139 tooltip = |
139 tooltip = |
140 GUI.tooltip_lines(List( |
140 GUI.tooltip_lines( |
141 "Automatic provers as space-separated list, e.g.", |
141 "Automatic provers as space-separated list, e.g.\ne spass remote_vampire") |
142 "", |
|
143 " e spass remote_vampire")) |
|
144 } |
142 } |
145 |
143 |
146 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
144 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
147 override def processKeyEvent(evt: KeyEvent) |
145 override def processKeyEvent(evt: KeyEvent) |
148 { |
146 { |