equal
deleted
inserted
replaced
134 private def clicked { |
134 private def clicked { |
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 = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")" |
139 tooltip = |
|
140 GUI.tooltip_lines(List( |
|
141 "Automatic provers as space-separated list, e.g.", |
|
142 "", |
|
143 " e spass remote_vampire")) |
140 } |
144 } |
141 |
145 |
142 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
146 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { |
143 override def processKeyEvent(evt: KeyEvent) |
147 override def processKeyEvent(evt: KeyEvent) |
144 { |
148 { |