64 |
64 |
65 override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = |
65 override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = |
66 { |
66 { |
67 Swing_Thread.require() |
67 Swing_Thread.require() |
68 |
68 |
69 if (snapshot.is_outdated) None |
69 val text_area = view.getTextArea |
70 else { |
70 PIDE.document_view(text_area) match { |
71 val text_area = view.getTextArea |
71 case Some(doc_view) => |
72 PIDE.document_view(text_area) match { |
72 val node = snapshot.version.nodes(doc_view.model.node_name) |
73 case Some(doc_view) => |
73 val caret = snapshot.revert(text_area.getCaretPosition) |
74 val node = snapshot.version.nodes(doc_view.model.node_name) |
74 if (caret < text_area.getBuffer.getLength) { |
75 val caret = text_area.getCaretPosition |
75 val caret_commands = node.command_range(caret) |
76 if (caret < text_area.getBuffer.getLength) { |
76 if (caret_commands.hasNext) { |
77 val caret_commands = node.command_range(caret) |
77 val (cmd0, _) = caret_commands.next |
78 if (caret_commands.hasNext) { |
78 node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored) |
79 val (cmd0, _) = caret_commands.next |
|
80 node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored) |
|
81 } |
|
82 else None |
|
83 } |
79 } |
84 else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
80 else None |
85 case None => None |
81 } |
86 } |
82 else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
|
83 case None => None |
87 } |
84 } |
88 } |
85 } |
89 |
86 |
90 |
87 |
91 /* overlays */ |
88 /* overlays */ |