author | wenzelm |
Sun, 08 Jan 2017 12:00:37 +0100 | |
changeset 64830 | 9bc44bef99e6 |
parent 64821 | 37bf7acf6a4b |
child 64833 | 0f410e3b1d20 |
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 |
|
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
13 |
import java.io.{File => JFile} |
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
14 |
|
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
15 |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
16 |
object VSCode_Rendering |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
17 |
{ |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
18 |
/* diagnostic messages */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
19 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
20 |
private val message_severity = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
21 |
Map( |
64762
cd545bec3fd0
clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents:
64759
diff
changeset
|
22 |
Markup.WRITELN -> Protocol.DiagnosticSeverity.Information, |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
23 |
Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
24 |
Markup.WARNING -> Protocol.DiagnosticSeverity.Warning, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
25 |
Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
26 |
Markup.ERROR -> Protocol.DiagnosticSeverity.Error, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
27 |
Markup.BAD -> Protocol.DiagnosticSeverity.Error) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
28 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
29 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
30 |
/* markup elements */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
31 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
32 |
private val diagnostics_elements = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
33 |
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
34 |
Markup.BAD) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
35 |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
36 |
private val hyperlink_elements = |
64652 | 37 |
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION) |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
38 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
39 |
|
64649 | 40 |
class VSCode_Rendering( |
41 |
val model: Document_Model, |
|
42 |
snapshot: Document.Snapshot, |
|
64702 | 43 |
resources: VSCode_Resources) |
64704 | 44 |
extends Rendering(snapshot, resources.options, resources) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
45 |
{ |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
46 |
/* diagnostics */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
47 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
48 |
def diagnostics: List[Text.Info[Command.Results]] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
49 |
snapshot.cumulate[Command.Results]( |
64830 | 50 |
model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
51 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
52 |
case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body))) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
53 |
if body.nonEmpty => Some(res + (i -> msg)) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
54 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
55 |
case _ => None |
64802 | 56 |
}).filterNot(info => info.info.is_empty) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
57 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
58 |
val diagnostics_margin = options.int("vscode_diagnostics_margin") |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
59 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
60 |
def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
61 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
62 |
(for { |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
63 |
Text.Info(text_range, res) <- results.iterator |
64830 | 64 |
range = model.content.doc.range(text_range) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
65 |
(_, XML.Elem(Markup(name, _), body)) <- res.iterator |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
66 |
} yield { |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
67 |
val message = Pretty.string_of(body, margin = diagnostics_margin) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
68 |
val severity = VSCode_Rendering.message_severity.get(name) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
69 |
Protocol.Diagnostic(range, message, severity = severity) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
70 |
}).toList |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
71 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
72 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
73 |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
74 |
/* tooltips */ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
75 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
76 |
def tooltip_margin: Int = options.int("vscode_tooltip_margin") |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
77 |
def timing_threshold: Double = options.real("vscode_timing_threshold") |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
78 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
79 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
80 |
/* hyperlinks */ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
81 |
|
64667 | 82 |
def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) |
83 |
: Option[Line.Node_Range] = |
|
84 |
{ |
|
64775 | 85 |
for { |
64779 | 86 |
platform_path <- resources.source_file(source_name) |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
87 |
file <- |
64779 | 88 |
(try { Some(new JFile(platform_path).getCanonicalFile) } |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
89 |
catch { case ERROR(_) => None }) |
64775 | 90 |
} |
64667 | 91 |
yield { |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
92 |
Line.Node_Range(file.getPath, |
64779 | 93 |
resources.get_file_content(file) match { |
64667 | 94 |
case Some(text) if range.start > 0 => |
95 |
val chunk = Symbol.Text_Chunk(text) |
|
64706 | 96 |
val doc = Line.Document(text, resources.text_length) |
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64679
diff
changeset
|
97 |
doc.range(chunk.decode(range)) |
64667 | 98 |
case _ => |
99 |
Line.Range(Line.Position((line1 - 1) max 0)) |
|
100 |
}) |
|
101 |
} |
|
102 |
} |
|
103 |
||
104 |
def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = |
|
105 |
{ |
|
106 |
if (snapshot.is_outdated) None |
|
107 |
else |
|
108 |
for { |
|
109 |
start <- snapshot.find_command_position(id, range.start) |
|
110 |
stop <- snapshot.find_command_position(id, range.stop) |
|
111 |
} yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) |
|
112 |
} |
|
113 |
||
114 |
def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = |
|
115 |
pos match { |
|
116 |
case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
117 |
case Position.Item_Id(id, range) => hyperlink_command(id, range) |
|
118 |
case _ => None |
|
119 |
} |
|
120 |
||
121 |
def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = |
|
122 |
pos match { |
|
123 |
case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
124 |
case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) |
|
125 |
case _ => None |
|
126 |
} |
|
127 |
||
64651 | 128 |
def hyperlinks(range: Text.Range): List[Line.Node_Range] = |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
129 |
{ |
64651 | 130 |
snapshot.cumulate[List[Line.Node_Range]]( |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
131 |
range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
132 |
{ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
133 |
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
64759 | 134 |
val file = resources.append_file(snapshot.node_name.master_dir, name) |
64654 | 135 |
Some(Line.Node_Range(file) :: links) |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
136 |
|
64667 | 137 |
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
138 |
hyperlink_def_position(props).map(_ :: links) |
|
139 |
||
140 |
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
|
141 |
hyperlink_position(props).map(_ :: links) |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
142 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
143 |
case _ => None |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
144 |
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
145 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
146 |
} |