author | wenzelm |
Fri, 23 Dec 2016 20:06:54 +0100 | |
changeset 64668 | 39a6c88c059b |
parent 64667 | cdb0d559a24b |
child 64679 | b2bf280b7e13 |
permissions | -rw-r--r-- |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/VSCode/src/vscode_rendering.scala |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
3 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle/VSCode-specific implementation of quasi-abstract rendering and |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
5 |
markup interpretation. |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
6 |
*/ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
7 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.vscode |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
9 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
10 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
11 |
import isabelle._ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
12 |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
13 |
object VSCode_Rendering |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
14 |
{ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
15 |
private val hyperlink_elements = |
64652 | 16 |
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION) |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
17 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
18 |
|
64649 | 19 |
class VSCode_Rendering( |
20 |
val model: Document_Model, |
|
21 |
snapshot: Document.Snapshot, |
|
22 |
options: Options, |
|
64667 | 23 |
text_length: Length, |
64649 | 24 |
resources: Resources) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
25 |
extends Rendering(snapshot, options, resources) |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
26 |
{ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
27 |
/* tooltips */ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
28 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
29 |
def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
30 |
def timing_threshold: Double = options.real("vscode_timing_threshold") |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
31 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
32 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
33 |
/* hyperlinks */ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
34 |
|
64667 | 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 } |
|
64668 | 43 |
Line.Node_Range(File.platform_url(name), |
64667 | 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 |
||
64651 | 80 |
def hyperlinks(range: Text.Range): List[Line.Node_Range] = |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
81 |
{ |
64651 | 82 |
snapshot.cumulate[List[Line.Node_Range]]( |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
83 |
range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
84 |
{ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
85 |
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
64654 | 86 |
val file = resources.append_file_url(snapshot.node_name.master_dir, name) |
87 |
Some(Line.Node_Range(file) :: links) |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
88 |
|
64667 | 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) |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
94 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
95 |
case _ => None |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
96 |
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
97 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
98 |
} |