376 case Position.Def_Line_File(line, name) => |
376 case Position.Def_Line_File(line, name) => |
377 val offset = Position.Def_Offset.unapply(props) getOrElse 0 |
377 val offset = Position.Def_Offset.unapply(props) getOrElse 0 |
378 PIDE.editor.hyperlink_source_file(name, line, offset) |
378 PIDE.editor.hyperlink_source_file(name, line, offset) |
379 case Position.Def_Id_Offset(id, offset) => |
379 case Position.Def_Id_Offset(id, offset) => |
380 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
380 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
|
381 case Position.Def_Id(id) => |
|
382 PIDE.editor.hyperlink_command_id(snapshot, id) |
381 case _ => None |
383 case _ => None |
382 } |
384 } |
383 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
385 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
384 |
386 |
385 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
387 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
388 case Position.Line_File(line, name) => |
390 case Position.Line_File(line, name) => |
389 val offset = Position.Offset.unapply(props) getOrElse 0 |
391 val offset = Position.Offset.unapply(props) getOrElse 0 |
390 PIDE.editor.hyperlink_source_file(name, line, offset) |
392 PIDE.editor.hyperlink_source_file(name, line, offset) |
391 case Position.Id_Offset(id, offset) => |
393 case Position.Id_Offset(id, offset) => |
392 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
394 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
|
395 case Position.Id(id) => |
|
396 PIDE.editor.hyperlink_command_id(snapshot, id) |
393 case _ => None |
397 case _ => None |
394 } |
398 } |
395 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
399 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
396 |
400 |
397 case _ => None |
401 case _ => None |