14 { |
14 { |
15 private val hyperlink_elements = |
15 private val hyperlink_elements = |
16 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) |
16 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) |
17 } |
17 } |
18 |
18 |
19 class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources) |
19 class VSCode_Rendering( |
|
20 val model: Document_Model, |
|
21 snapshot: Document.Snapshot, |
|
22 options: Options, |
|
23 resources: Resources) |
20 extends Rendering(snapshot, options, resources) |
24 extends Rendering(snapshot, options, resources) |
21 { |
25 { |
22 /* tooltips */ |
26 /* tooltips */ |
23 |
27 |
24 def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
28 def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
25 def timing_threshold: Double = options.real("vscode_timing_threshold") |
29 def timing_threshold: Double = options.real("vscode_timing_threshold") |
26 |
30 |
27 |
31 |
28 /* hyperlinks */ |
32 /* hyperlinks */ |
29 |
33 |
30 def hyperlinks(range: Text.Range): List[(String, Line.Range)] = |
34 def hyperlinks(range: Text.Range): List[Line.Range_Node] = |
31 { |
35 { |
32 snapshot.cumulate[List[(String, Line.Range)]]( |
36 snapshot.cumulate[List[Line.Range_Node]]( |
33 range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
37 range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
34 { |
38 { |
35 case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
39 case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
36 Some((resolve_file_url(name), Line.Range.zero) :: links) |
40 Some(Line.Range_Node(Line.Range.zero, resolve_file_url(name)) :: links) |
37 |
41 |
38 /* FIXME |
42 /* FIXME |
39 case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) => |
43 case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) => |
40 Some(PIDE.editor.hyperlink_url(name) :: links) |
44 Some(PIDE.editor.hyperlink_url(name) :: links) |
41 |
45 |