--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 17:14:27 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 17:28:17 2017 +0200
@@ -71,6 +71,7 @@
rendering =>
def model: Document_Model = _model
+ def resources: VSCode_Resources = model.resources
/* completion */
@@ -136,7 +137,7 @@
range = model.content.doc.range(text_range)
(_, XML.Elem(Markup(name, _), body)) <- res.iterator
} yield {
- val message = model.resources.output_pretty_message(body)
+ val message = resources.output_pretty_message(body)
val severity = VSCode_Rendering.message_severity.get(name)
Protocol.Diagnostic(range, message, severity = severity)
}).toList
@@ -222,7 +223,7 @@
yield {
val range = model.content.doc.range(text_range)
Protocol.DecorationOpts(range,
- msgs.map(msg => Protocol.MarkedString(model.resources.output_pretty_tooltip(msg))))
+ msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
}
Protocol.Decoration(decoration.typ, content)
}
@@ -239,7 +240,7 @@
: Option[Line.Node_Range] =
{
for {
- platform_path <- model.resources.source_file(source_name)
+ platform_path <- resources.source_file(source_name)
file <-
(try { Some(new JFile(platform_path).getCanonicalFile) }
catch { case ERROR(_) => None })
@@ -247,7 +248,7 @@
yield {
Line.Node_Range(file.getPath,
if (range.start > 0) {
- model.resources.get_file_content(file) match {
+ resources.get_file_content(file) match {
case Some(text) =>
val chunk = Symbol.Text_Chunk(text)
val doc = Line.Document(text)
@@ -302,7 +303,7 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val iterator =
for {
- Text.Info(entry_range, (entry, model)) <- model.resources.bibtex_entries_iterator
+ Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
if entry == name
} yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
--- a/src/Tools/VSCode/src/vscode_spell_checker.scala Tue Jun 20 17:14:27 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_spell_checker.scala Tue Jun 20 17:28:17 2017 +0200
@@ -17,7 +17,7 @@
val model = rendering.model
val ranges =
(for {
- spell_checker <- model.resources.spell_checker.get.iterator
+ spell_checker <- rendering.resources.spell_checker.get.iterator
spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
text <- model.try_get_text(spell_range).iterator
info <- spell_checker.marked_words(spell_range.start, text).iterator
@@ -26,14 +26,13 @@
}
def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] =
- rendering.model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
+ rendering.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] =
{
- val model = rendering.model
val result =
for {
- spell_checker <- model.resources.spell_checker.get
+ spell_checker <- rendering.resources.spell_checker.get
range = rendering.before_caret_range(caret)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} yield (spell_checker, word)
@@ -45,7 +44,7 @@
Protocol.CompletionItem(
label = command.title,
text = Some(""),
- range = Some(model.content.doc.range(Text.Range(caret))),
+ range = Some(rendering.model.content.doc.range(Text.Range(caret))),
command = Some(command))
val update_items =