equal
deleted
inserted
replaced
55 } |
55 } |
56 |
56 |
57 private def apply_query(text: String) |
57 private def apply_query(text: String) |
58 { |
58 { |
59 Swing_Thread.require() |
59 Swing_Thread.require() |
|
60 |
|
61 Document_View(view.getTextArea) match { |
|
62 case Some(doc_view) => |
|
63 val snapshot = doc_view.model.snapshot() |
|
64 current_location = snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) |
|
65 case None => |
|
66 } |
60 } |
67 } |
61 |
68 |
62 private def locate_query() |
69 private def locate_query() |
63 { |
70 { |
64 Swing_Thread.require() |
71 Swing_Thread.require() |
|
72 |
|
73 current_location match { |
|
74 case Some(command) => |
|
75 val snapshot = PIDE.session.snapshot(command.node_name) |
|
76 val commands = snapshot.node.commands |
|
77 if (commands.contains(command)) { |
|
78 val sources = commands.iterator.takeWhile(_ != command).map(_.source) |
|
79 val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
|
80 Hyperlink(command.node_name.node, line, column).follow(view) |
|
81 } |
|
82 case None => |
|
83 } |
65 } |
84 } |
66 |
85 |
67 |
86 |
68 /* main actor */ |
87 /* main actor */ |
69 |
88 |
88 { |
107 { |
89 Swing_Thread.require() |
108 Swing_Thread.require() |
90 |
109 |
91 PIDE.session.global_options += main_actor |
110 PIDE.session.global_options += main_actor |
92 PIDE.session.commands_changed += main_actor |
111 PIDE.session.commands_changed += main_actor |
93 handle_output() |
112 handle_resize() |
94 } |
113 } |
95 |
114 |
96 override def exit() |
115 override def exit() |
97 { |
116 { |
98 Swing_Thread.require() |
117 Swing_Thread.require() |