154 } |
154 } |
155 |
155 |
156 override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink = |
156 override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink = |
157 new Hyperlink { def follow(view: View) = goto(view, name, line, column) } |
157 new Hyperlink { def follow(view: View) = goto(view, name, line, column) } |
158 |
158 |
159 override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0) |
159 override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0) |
160 : Option[Hyperlink] = |
160 : Option[Hyperlink] = |
161 { |
161 { |
162 if (snapshot.is_outdated) None |
162 if (snapshot.is_outdated) None |
163 else { |
163 else { |
164 snapshot.state.find_command(snapshot.version, command.id) match { |
164 snapshot.state.find_command(snapshot.version, command.id) match { |
165 case None => None |
165 case None => None |
166 case Some((node, _)) => |
166 case Some((node, _)) => |
167 val file_name = command.node_name.node |
167 val file_name = command.node_name.node |
168 val sources = |
168 val sources = |
169 node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
169 node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
170 (if (offset == 0) Iterator.empty |
170 (if (raw_offset == 0) Iterator.empty |
171 else Iterator.single(command.source(Text.Range(0, command.decode(offset))))) |
171 else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset))))) |
172 val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
172 val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
173 Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } }) |
173 Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } }) |
174 } |
174 } |
175 } |
175 } |
176 } |
176 } |