equal
deleted
inserted
replaced
271 } |
271 } |
272 } |
272 } |
273 |
273 |
274 |
274 |
275 /* caret handling */ |
275 /* caret handling */ |
276 |
|
277 def selected_command(): Option[Command] = |
|
278 { |
|
279 Swing_Thread.require() |
|
280 model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1) |
|
281 } |
|
282 |
276 |
283 private val delay_caret_update = |
277 private val delay_caret_update = |
284 Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) { |
278 Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) { |
285 session.caret_focus.event(Session.Caret_Focus) |
279 session.caret_focus.event(Session.Caret_Focus) |
286 } |
280 } |