author | wenzelm |
Fri, 09 Jun 2017 21:57:30 +0200 | |
changeset 66055 | 07175635f78c |
parent 66054 | fb0eea226a4d |
child 66057 | b8555ca0af07 |
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 |
|
65913 | 15 |
import scala.annotation.tailrec |
16 |
||
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
17 |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
18 |
object VSCode_Rendering |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
19 |
{ |
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
20 |
/* decorations */ |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
21 |
|
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
22 |
private def color_decorations(prefix: String, types: Set[Rendering.Color.Value], |
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
23 |
colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] = |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
24 |
{ |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
25 |
val color_ranges = |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
26 |
(Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
27 |
case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
28 |
} |
65105 | 29 |
types.toList.map(c => |
65140 | 30 |
Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) |
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
31 |
} |
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
32 |
|
65176 | 33 |
private val background_colors = |
34 |
Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result - |
|
35 |
Rendering.Color.entity |
|
36 |
||
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
37 |
private val dotted_colors = |
65134
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
38 |
Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) |
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
39 |
|
65104
66b19d05dcee
decorations for background and foreground colors;
wenzelm
parents:
65095
diff
changeset
|
40 |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
41 |
/* diagnostic messages */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
42 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
43 |
private val message_severity = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
44 |
Map( |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
45 |
Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning, |
65095 | 46 |
Markup.ERROR -> Protocol.DiagnosticSeverity.Error) |
64679
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 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
49 |
/* markup elements */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
50 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
51 |
private val diagnostics_elements = |
65134
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
52 |
Markup.Elements(Markup.LEGACY, Markup.ERROR) |
65095 | 53 |
|
65176 | 54 |
private val background_elements = |
55 |
Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements |
|
56 |
||
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
57 |
private val dotted_elements = |
65134
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
58 |
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) |
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
59 |
|
65134
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
60 |
val tooltip_elements = |
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
61 |
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++ |
511bf19348d3
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents:
65122
diff
changeset
|
62 |
Rendering.tooltip_elements |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
63 |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
64 |
private val hyperlink_elements = |
64833 | 65 |
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION) |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
66 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
67 |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
68 |
class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot) |
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
69 |
extends Rendering(snapshot, model.resources.options, model.session) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
70 |
{ |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
71 |
rendering => |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
72 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
73 |
|
64877 | 74 |
/* completion */ |
75 |
||
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
76 |
def before_caret_range(caret: Text.Offset): Text.Range = |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
77 |
{ |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
78 |
val former_caret = snapshot.revert(caret) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
79 |
snapshot.convert(Text.Range(former_caret - 1, former_caret)) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
80 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
81 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
82 |
def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] = |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
83 |
{ |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
84 |
val caret_range = before_caret_range(caret) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
85 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
86 |
val history = Completion.History.empty |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
87 |
val doc = model.content.doc |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
88 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
89 |
val syntax_completion = |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
90 |
{ |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
91 |
val syntax = model.syntax() |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
92 |
val context = language_context(caret_range) getOrElse syntax.language_context |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
93 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
94 |
val line = caret_pos.line |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
95 |
doc.offset(Line.Position(line)) match { |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
96 |
case Some(line_start) => |
66055 | 97 |
syntax.completion.complete(history, unicode = false, explicit = true, |
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
98 |
line_start, doc.lines(line).text, caret - line_start, context) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
99 |
case None => None |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
100 |
} |
64877 | 101 |
} |
102 |
||
66054
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
103 |
val (no_completion, semantic_completion) = |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
104 |
rendering.semantic_completion_result( |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
105 |
history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_)) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
106 |
|
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
107 |
if (no_completion) Nil |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
108 |
else { |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
109 |
Completion.Result.merge(history, semantic_completion, syntax_completion) match { |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
110 |
case None => Nil |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
111 |
case Some(result) => |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
112 |
result.items.map(item => |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
113 |
Protocol.CompletionItem( |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
114 |
label = item.replacement, |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
115 |
detail = Some(item.description.mkString(" ")), |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
116 |
range = Some(doc.range(item.range)))) |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
117 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
118 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
119 |
} |
fb0eea226a4d
more uniform syntax_completion + semantic_completion;
wenzelm
parents:
65925
diff
changeset
|
120 |
|
64877 | 121 |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
122 |
/* diagnostics */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
123 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
124 |
def diagnostics: List[Text.Info[Command.Results]] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
125 |
snapshot.cumulate[Command.Results]( |
64830 | 126 |
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
|
127 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
128 |
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
|
129 |
if body.nonEmpty => Some(res + (i -> msg)) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
130 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
131 |
case _ => None |
64802 | 132 |
}).filterNot(info => info.info.is_empty) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
133 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
134 |
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
|
135 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
136 |
(for { |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
137 |
Text.Info(text_range, res) <- results.iterator |
64830 | 138 |
range = model.content.doc.range(text_range) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
139 |
(_, XML.Elem(Markup(name, _), body)) <- res.iterator |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
140 |
} yield { |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
141 |
val message = model.resources.output_pretty_message(body) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
142 |
val severity = VSCode_Rendering.message_severity.get(name) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
143 |
Protocol.Diagnostic(range, message, severity = severity) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
144 |
}).toList |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
145 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
146 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset
|
147 |
|
65146 | 148 |
/* text color */ |
149 |
||
150 |
def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = |
|
151 |
{ |
|
152 |
snapshot.select(range, Rendering.text_color_elements, _ => |
|
153 |
{ |
|
65174
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
65173
diff
changeset
|
154 |
case Text.Info(_, XML.Elem(Markup(name, props), _)) => |
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
65173
diff
changeset
|
155 |
if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None |
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
65173
diff
changeset
|
156 |
else Rendering.text_color.get(name) |
65146 | 157 |
}) |
158 |
} |
|
159 |
||
160 |
||
65913 | 161 |
/* text overview color */ |
162 |
||
163 |
private sealed case class Color_Info( |
|
164 |
color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int) |
|
165 |
||
166 |
def text_overview_color: List[Text.Info[Rendering.Color.Value]] = |
|
167 |
{ |
|
168 |
@tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info]) |
|
169 |
: List[Text.Info[Rendering.Color.Value]] = |
|
170 |
{ |
|
171 |
if (lines.nonEmpty) { |
|
172 |
val end_offset = offset + lines.head.text.length |
|
173 |
val colors1 = |
|
174 |
(overview_color(Text.Range(offset, end_offset)), colors) match { |
|
175 |
case (Some(color), old :: rest) if color == old.color && line == old.end_line => |
|
176 |
old.copy(end_offset = end_offset, end_line = line + 1) :: rest |
|
177 |
case (Some(color), _) => |
|
178 |
Color_Info(color, offset, end_offset, line + 1) :: colors |
|
179 |
case (None, _) => colors |
|
180 |
} |
|
181 |
loop(end_offset + 1, line + 1, lines.tail, colors1) |
|
182 |
} |
|
183 |
else { |
|
184 |
colors.reverse.map(info => |
|
185 |
Text.Info(Text.Range(info.offset, info.end_offset), info.color)) |
|
186 |
} |
|
187 |
} |
|
188 |
loop(0, 0, model.content.doc.lines, Nil) |
|
189 |
} |
|
190 |
||
191 |
||
65122
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
192 |
/* dotted underline */ |
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
193 |
|
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
194 |
def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = |
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
195 |
message_underline_color(VSCode_Rendering.dotted_elements, range) |
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
196 |
|
1edb570f5b17
decorations for dotted underline: less intrusive;
wenzelm
parents:
65120
diff
changeset
|
197 |
|
65142 | 198 |
/* spell checker */ |
199 |
||
200 |
def spell_checker: Document_Model.Decoration = |
|
201 |
{ |
|
202 |
val ranges = |
|
203 |
(for { |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
204 |
spell_checker <- model.resources.spell_checker.get.iterator |
65142 | 205 |
spell_range <- spell_checker_ranges(model.content.text_range).iterator |
206 |
text <- model.content.try_get_text(spell_range).iterator |
|
207 |
info <- spell_checker.marked_words(spell_range.start, text).iterator |
|
208 |
} yield info.range).toList |
|
209 |
Document_Model.Decoration.ranges("spell_checker", ranges) |
|
210 |
} |
|
211 |
||
212 |
||
65095 | 213 |
/* decorations */ |
214 |
||
65120
db6cc23fcf33
proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
wenzelm
parents:
65107
diff
changeset
|
215 |
def decorations: List[Document_Model.Decoration] = // list of canonical length and order |
65925 | 216 |
Par_List.map((f: () => List[Document_Model.Decoration]) => f(), |
217 |
List( |
|
218 |
() => |
|
219 |
VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors, |
|
220 |
background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)), |
|
221 |
() => |
|
222 |
VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, |
|
223 |
foreground(model.content.text_range)), |
|
224 |
() => |
|
225 |
VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, |
|
226 |
text_color(model.content.text_range)), |
|
227 |
() => |
|
228 |
VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors, |
|
229 |
text_overview_color), |
|
230 |
() => |
|
231 |
VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, |
|
232 |
dotted(model.content.text_range)))).flatten ::: |
|
65142 | 233 |
List(spell_checker) |
65095 | 234 |
|
235 |
def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = |
|
236 |
{ |
|
237 |
val content = |
|
65105 | 238 |
for (Text.Info(text_range, msgs) <- decoration.content) |
65095 | 239 |
yield { |
240 |
val range = model.content.doc.range(text_range) |
|
65173 | 241 |
Protocol.DecorationOpts(range, |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
242 |
msgs.map(msg => Protocol.MarkedString(model.resources.output_pretty_tooltip(msg)))) |
65095 | 243 |
} |
244 |
Protocol.Decoration(decoration.typ, content) |
|
245 |
} |
|
246 |
||
247 |
||
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
248 |
/* tooltips */ |
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
249 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
250 |
def timing_threshold: Double = options.real("vscode_timing_threshold") |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
251 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
252 |
|
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
253 |
/* hyperlinks */ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
254 |
|
64667 | 255 |
def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) |
256 |
: Option[Line.Node_Range] = |
|
257 |
{ |
|
64775 | 258 |
for { |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
259 |
platform_path <- model.resources.source_file(source_name) |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
260 |
file <- |
64779 | 261 |
(try { Some(new JFile(platform_path).getCanonicalFile) } |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
262 |
catch { case ERROR(_) => None }) |
64775 | 263 |
} |
64667 | 264 |
yield { |
64778
7884a19de325
proper interpretation of Resources.source_file as platform file;
wenzelm
parents:
64777
diff
changeset
|
265 |
Line.Node_Range(file.getPath, |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
266 |
if (range.start > 0) { |
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
267 |
model.resources.get_file_content(file) match { |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
268 |
case Some(text) => |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
269 |
val chunk = Symbol.Text_Chunk(text) |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65176
diff
changeset
|
270 |
val doc = Line.Document(text) |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
271 |
doc.range(chunk.decode(range)) |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
272 |
case _ => |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
273 |
Line.Range(Line.Position((line1 - 1) max 0)) |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
274 |
} |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
275 |
} |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64833
diff
changeset
|
276 |
else Line.Range(Line.Position((line1 - 1) max 0))) |
64667 | 277 |
} |
278 |
} |
|
279 |
||
280 |
def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = |
|
281 |
{ |
|
282 |
if (snapshot.is_outdated) None |
|
283 |
else |
|
284 |
for { |
|
285 |
start <- snapshot.find_command_position(id, range.start) |
|
286 |
stop <- snapshot.find_command_position(id, range.stop) |
|
287 |
} yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) |
|
288 |
} |
|
289 |
||
290 |
def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = |
|
291 |
pos match { |
|
292 |
case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
293 |
case Position.Item_Id(id, range) => hyperlink_command(id, range) |
|
294 |
case _ => None |
|
295 |
} |
|
296 |
||
297 |
def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = |
|
298 |
pos match { |
|
299 |
case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) |
|
300 |
case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) |
|
301 |
case _ => None |
|
302 |
} |
|
303 |
||
64651 | 304 |
def hyperlinks(range: Text.Range): List[Line.Node_Range] = |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
305 |
{ |
64651 | 306 |
snapshot.cumulate[List[Line.Node_Range]]( |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
307 |
range, Nil, VSCode_Rendering.hyperlink_elements, _ => |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
308 |
{ |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
309 |
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => |
65488 | 310 |
val file = perhaps_append_file(snapshot.node_name, name) |
64654 | 311 |
Some(Line.Node_Range(file) :: links) |
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
312 |
|
64667 | 313 |
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
314 |
hyperlink_def_position(props).map(_ :: links) |
|
315 |
||
316 |
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
|
317 |
hyperlink_position(props).map(_ :: links) |
|
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
318 |
|
64833 | 319 |
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => |
320 |
val iterator = |
|
321 |
for { |
|
65213
51c0f094dc02
proper local debugger state, depending on session;
wenzelm
parents:
65196
diff
changeset
|
322 |
Text.Info(entry_range, (entry, model)) <- model.resources.bibtex_entries_iterator |
64833 | 323 |
if entry == name |
324 |
} yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) |
|
325 |
if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _)) |
|
326 |
||
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
327 |
case _ => None |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
328 |
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } |
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset
|
329 |
} |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset
|
330 |
} |