29 def timing_threshold: Double = options.real("vscode_timing_threshold") |
30 def timing_threshold: Double = options.real("vscode_timing_threshold") |
30 |
31 |
31 |
32 |
32 /* hyperlinks */ |
33 /* hyperlinks */ |
33 |
34 |
|
35 def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) |
|
36 : Option[Line.Node_Range] = |
|
37 { |
|
38 for (name <- resources.source_file(source_name)) |
|
39 yield { |
|
40 val opt_text = |
|
41 try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models |
|
42 catch { case ERROR(_) => None } |
|
43 Line.Node_Range(name, |
|
44 opt_text match { |
|
45 case Some(text) if range.start > 0 => |
|
46 val chunk = Symbol.Text_Chunk(text) |
|
47 val doc = Line.Document(text) |
|
48 def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length) |
|
49 Line.Range(position(range.start), position(range.stop)) |
|
50 case _ => |
|
51 Line.Range(Line.Position((line1 - 1) max 0)) |
|
52 }) |
|
53 } |
|
54 } |
|
55 |
|
56 def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = |
|
57 { |
|
58 if (snapshot.is_outdated) None |
|
59 else |
|
60 for { |
|
61 start <- snapshot.find_command_position(id, range.start) |
|
62 stop <- snapshot.find_command_position(id, range.stop) |
|
63 } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) |
|
64 } |
|
65 |
|
66 def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = |
|
67 pos match { |
|
68 case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
69 case Position.Item_Id(id, range) => hyperlink_command(id, range) |
|
70 case _ => None |
|
71 } |
|
72 |
|
73 def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = |
|
74 pos match { |
|
75 case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
76 case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) |
|
77 case _ => None |
|
78 } |
|
79 |
34 def hyperlinks(range: Text.Range): List[Line.Node_Range] = |
80 def hyperlinks(range: Text.Range): List[Line.Node_Range] = |
35 { |
81 { |
36 snapshot.cumulate[List[Line.Node_Range]]( |
82 snapshot.cumulate[List[Line.Node_Range]]( |
37 range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
83 range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
38 { |
84 { |
39 case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
85 case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
40 val file = resources.append_file_url(snapshot.node_name.master_dir, name) |
86 val file = resources.append_file_url(snapshot.node_name.master_dir, name) |
41 Some(Line.Node_Range(file) :: links) |
87 Some(Line.Node_Range(file) :: links) |
42 |
88 |
43 // FIXME more cases |
89 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
|
90 hyperlink_def_position(props).map(_ :: links) |
|
91 |
|
92 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
|
93 hyperlink_position(props).map(_ :: links) |
44 |
94 |
45 case _ => None |
95 case _ => None |
46 }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } |
96 }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } |
47 } |
97 } |
48 } |
98 } |