282 override def hyperlink_command( |
282 override def hyperlink_command( |
283 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
283 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
284 : Option[Hyperlink] = |
284 : Option[Hyperlink] = |
285 { |
285 { |
286 if (snapshot.is_outdated) None |
286 if (snapshot.is_outdated) None |
287 else { |
287 else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _)) |
288 snapshot.state.find_command(snapshot.version, id) match { |
|
289 case None => None |
|
290 case Some((node, command)) => |
|
291 val name = command.node_name.node |
|
292 val sources_iterator = |
|
293 node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
|
294 (if (offset == 0) Iterator.empty |
|
295 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) |
|
296 val pos = (Line.Position.zero /: sources_iterator)(_.advance(_)) |
|
297 Some(hyperlink_file(focus, Line.Node_Position(name, pos))) |
|
298 } |
|
299 } |
|
300 } |
288 } |
301 |
289 |
302 def is_hyperlink_position(snapshot: Document.Snapshot, |
290 def is_hyperlink_position(snapshot: Document.Snapshot, |
303 text_offset: Text.Offset, pos: Position.T): Boolean = |
291 text_offset: Text.Offset, pos: Position.T): Boolean = |
304 { |
292 { |
305 pos match { |
293 pos match { |
306 case Position.Item_Id(id, offset) if offset > 0 => |
294 case Position.Item_Id(id, offset) if offset > 0 => |
307 snapshot.state.find_command(snapshot.version, id) match { |
295 snapshot.find_command(id) match { |
308 case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => |
296 case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => |
309 node.command_start(command) match { |
297 node.command_start(command) match { |
310 case Some(start) => text_offset == start + command.chunk.decode(offset) |
298 case Some(start) => text_offset == start + command.chunk.decode(offset) |
311 case None => false |
299 case None => false |
312 } |
300 } |