139 def docked_protocol(view: View): Option[Protocol_Dockable] = |
139 def docked_protocol(view: View): Option[Protocol_Dockable] = |
140 wm(view).getDockableWindow("isabelle-protocol") match { |
140 wm(view).getDockableWindow("isabelle-protocol") match { |
141 case dockable: Protocol_Dockable => Some(dockable) |
141 case dockable: Protocol_Dockable => Some(dockable) |
142 case _ => None |
142 case _ => None |
143 } |
143 } |
144 |
|
145 |
|
146 /* convenience actions */ |
|
147 |
|
148 private def user_input(text_area: JEditTextArea, s1: String, s2: String = "") |
|
149 { |
|
150 s1.foreach(text_area.userInput(_)) |
|
151 s2.foreach(text_area.userInput(_)) |
|
152 s2.foreach(_ => text_area.goToPrevCharacter(false)) |
|
153 } |
|
154 |
|
155 def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded) |
|
156 def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded) |
|
157 def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded) |
|
158 def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded) |
|
159 def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) |
|
160 def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) |
|
161 def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded) |
|
162 |
|
163 def check_buffer(buffer: Buffer) |
|
164 { |
|
165 document_model(buffer) match { |
|
166 case None => |
|
167 case Some(model) => model.full_perspective() |
|
168 } |
|
169 } |
|
170 |
|
171 def cancel_execution() { session.cancel_execution() } |
|
172 } |
144 } |
173 |
145 |
174 |
146 |
175 class Plugin extends EBPlugin |
147 class Plugin extends EBPlugin |
176 { |
148 { |