--- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 18:12:41 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 20:49:54 2012 +0200
@@ -274,12 +274,6 @@
/* caret handling */
- def selected_command(): Option[Command] =
- {
- Swing_Thread.require()
- model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
- }
-
private val delay_caret_update =
Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
session.caret_focus.event(Session.Caret_Focus)