# HG changeset patch # User wenzelm # Date 1606590886 -3600 # Node ID 4519eeefe3b5337125f9db518b4014914a2a7b99 # Parent 0421805400683880be1051b7021161aa90a05f14 avoid conflicting base names; diff -r 042180540068 -r 4519eeefe3b5 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Pure/System/isabelle_tool.scala Sat Nov 28 20:14:46 2020 +0100 @@ -167,7 +167,7 @@ Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.vscode.Grammar.isabelle_tool, - isabelle.vscode.Server.isabelle_tool) + isabelle.vscode.Language_Server.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_CSDP.isabelle_tool, diff -r 042180540068 -r 4519eeefe3b5 src/Pure/build-jars --- a/src/Pure/build-jars Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Pure/build-jars Sat Nov 28 20:14:46 2020 +0100 @@ -204,13 +204,13 @@ src/Tools/Graphview/tree_panel.scala src/Tools/VSCode/src/build_vscode.scala src/Tools/VSCode/src/channel.scala - src/Tools/VSCode/src/document_model.scala src/Tools/VSCode/src/dynamic_output.scala src/Tools/VSCode/src/grammar.scala + src/Tools/VSCode/src/language_server.scala + src/Tools/VSCode/src/lsp.scala src/Tools/VSCode/src/preview_panel.scala - src/Tools/VSCode/src/protocol.scala - src/Tools/VSCode/src/server.scala src/Tools/VSCode/src/state_panel.scala + src/Tools/VSCode/src/vscode_model.scala src/Tools/VSCode/src/vscode_rendering.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/VSCode/src/vscode_spell_checker.scala diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/channel.scala Sat Nov 28 20:14:46 2020 +0100 @@ -50,7 +50,7 @@ case Value.Int(n) if n >= 0 => val msg = read_content(n) val json = JSON.parse(msg) - Protocol.Message.log("IN: " + n, json, log, verbose) + LSP.Message.log("IN: " + n, json, log, verbose) Some(json) case _ => error("Bad Content-Length: " + s) } @@ -68,7 +68,7 @@ val n = content.length val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n") - Protocol.Message.log("OUT: " + n, json, log, verbose) + LSP.Message.log("OUT: " + n, json, log, verbose) out.synchronized { out.write(header) out.write(content) @@ -80,15 +80,15 @@ /* display message */ def display_message(message_type: Int, msg: String, show: Boolean = true): Unit = - write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show)) + write(LSP.DisplayMessage(message_type, Output.clean_yxml(msg), show)) - def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) } - def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) } - def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) } + def error_message(msg: String) { display_message(LSP.MessageType.Error, msg, true) } + def warning(msg: String) { display_message(LSP.MessageType.Warning, msg, true) } + def writeln(msg: String) { display_message(LSP.MessageType.Info, msg, true) } - def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) } - def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) } - def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) } + def log_error_message(msg: String) { display_message(LSP.MessageType.Error, msg, false) } + def log_warning(msg: String) { display_message(LSP.MessageType.Warning, msg, false) } + def log_writeln(msg: String) { display_message(LSP.MessageType.Info, msg, false) } object Error_Logger extends Logger { diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sat Nov 28 17:38:03 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,245 +0,0 @@ -/* Title: Tools/VSCode/src/document_model.scala - Author: Makarius - -Document model for line-oriented text. -*/ - -package isabelle.vscode - - -import isabelle._ - -import java.io.{File => JFile} - - -object Document_Model -{ - /* decorations */ - - object Decoration - { - def empty(typ: String): Decoration = Decoration(typ, Nil) - - def ranges(typ: String, ranges: List[Text.Range]): Decoration = - Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) - } - sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) - - - /* content */ - - object Content - { - val empty: Content = Content(Line.Document.empty) - } - - sealed case class Content(doc: Line.Document) - { - override def toString: String = doc.toString - def text_length: Text.Offset = doc.text_length - def text_range: Text.Range = doc.text_range - def text: String = doc.text - - lazy val bytes: Bytes = Bytes(text) - lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) - lazy val bibtex_entries: List[Text.Info[String]] = - try { Bibtex.entries(text) } - catch { case ERROR(_) => Nil } - - def recode_symbols: List[Protocol.TextEdit] = - (for { - (line, l) <- doc.lines.iterator.zipWithIndex - text1 = Symbol.encode(line.text) - if (line.text != text1) - } yield { - val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length)) - Protocol.TextEdit(range, text1) - }).toList - } - - def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = - Document_Model(session, editor, node_name, Content.empty, - node_required = File_Format.registry.is_theory(node_name)) -} - -sealed case class Document_Model( - session: Session, - editor: Server.Editor, - node_name: Document.Node.Name, - content: Document_Model.Content, - version: Option[Long] = None, - external_file: Boolean = false, - node_required: Boolean = false, - last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, - pending_edits: List[Text.Edit] = Nil, - published_diagnostics: List[Text.Info[Command.Results]] = Nil, - published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model -{ - model => - - - /* content */ - - def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) - - def set_version(new_version: Long): Document_Model = copy(version = Some(new_version)) - - - /* external file */ - - def external(b: Boolean): Document_Model = copy(external_file = b) - - def node_visible: Boolean = !external_file - - - /* header */ - - def node_header: Document.Node.Header = - resources.special_header(node_name) getOrElse - resources.check_thy_reader(node_name, Scan.char_reader(content.text)) - - - /* perspective */ - - def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position]) - : (Boolean, Document.Node.Perspective_Text) = - { - if (is_theory) { - val snapshot = model.snapshot() - - val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 - val caret_range = - if (caret_perspective != 0) { - caret match { - case Some(pos) => - val doc = content.doc - val pos1 = Line.Position((pos.line - caret_perspective) max 0) - val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length) - Text.Range(doc.offset(pos1).get, doc.offset(pos2).get) - case None => Text.Range.offside - } - } - else if (node_visible) content.text_range - else Text.Range.offside - - val text_perspective = - if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) - Text.Perspective.full - else - content.text_range.try_restrict(caret_range) match { - case Some(range) => Text.Perspective(List(range)) - case None => Text.Perspective.empty - } - - val overlays = editor.node_overlays(node_name) - - (snapshot.node.load_commands_changed(doc_blobs), - Document.Node.Perspective(node_required, text_perspective, overlays)) - } - else (false, Document.Node.no_perspective_text) - } - - - /* blob */ - - def get_blob: Option[Document.Blob] = - if (is_theory) None - else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) - - - /* bibtex entries */ - - def bibtex_entries: List[Text.Info[String]] = - model.content.bibtex_entries - - - /* edits */ - - def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] = - { - val insert = Line.normalize(text) - range match { - case None => - Text.Edit.replace(0, content.text, insert) match { - case Nil => None - case edits => - val content1 = Document_Model.Content(Line.Document(insert)) - Some(copy(content = content1, pending_edits = pending_edits ::: edits)) - } - case Some(remove) => - content.doc.change(remove, insert) match { - case None => error("Failed to apply document change: " + remove) - case Some((Nil, _)) => None - case Some((edits, doc1)) => - val content1 = Document_Model.Content(doc1) - Some(copy(content = content1, pending_edits = pending_edits ::: edits)) - } - } - } - - def flush_edits( - unicode_symbols: Boolean, - doc_blobs: Document.Blobs, - file: JFile, - caret: Option[Line.Position]) - : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] = - { - val workspace_edits = - if (unicode_symbols && version.isDefined) { - val edits = content.recode_symbols - if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits)) - else Nil - } - else Nil - - val (reparse, perspective) = node_perspective(doc_blobs, caret) - if (reparse || pending_edits.nonEmpty || last_perspective != perspective || - workspace_edits.nonEmpty) - { - val prover_edits = node_edits(node_header, pending_edits, perspective) - val edits = (workspace_edits, prover_edits) - Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) - } - else None - } - - - /* publish annotations */ - - def publish(rendering: VSCode_Rendering): - (Option[List[Text.Info[Command.Results]]], Option[List[Document_Model.Decoration]], Document_Model) = - { - val diagnostics = rendering.diagnostics - val decorations = - if (node_visible) rendering.decorations - else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) } - - val changed_diagnostics = - if (diagnostics == published_diagnostics) None else Some(diagnostics) - val changed_decorations = - if (decorations == published_decorations) None - else if (published_decorations.isEmpty) Some(decorations) - else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) - - (changed_diagnostics, changed_decorations, - copy(published_diagnostics = diagnostics, published_decorations = decorations)) - } - - - /* prover session */ - - def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] - - def is_stable: Boolean = pending_edits.isEmpty - def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) - - def rendering(snapshot: Document.Snapshot): VSCode_Rendering = - new VSCode_Rendering(snapshot, model) - def rendering(): VSCode_Rendering = rendering(snapshot()) - - - /* syntax */ - - def syntax(): Outer_Syntax = - if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty -} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/dynamic_output.scala --- a/src/Tools/VSCode/src/dynamic_output.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/dynamic_output.scala Sat Nov 28 20:14:46 2020 +0100 @@ -35,18 +35,18 @@ else this } if (st1.output != output) { - channel.write(Protocol.Dynamic_Output( + channel.write(LSP.Dynamic_Output( resources.output_pretty_message(Pretty.separate(st1.output)))) } st1 } } - def apply(server: Server): Dynamic_Output = new Dynamic_Output(server) + def apply(server: Language_Server): Dynamic_Output = new Dynamic_Output(server) } -class Dynamic_Output private(server: Server) +class Dynamic_Output private(server: Language_Server) { private val state = Synchronized(Dynamic_Output.State()) diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/language_server.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/language_server.scala Sat Nov 28 20:14:46 2020 +0100 @@ -0,0 +1,559 @@ +/* Title: Tools/VSCode/src/language_server.scala + Author: Makarius + +Server for VS Code Language Server Protocol 2.0/3.0, see also +https://github.com/Microsoft/language-server-protocol +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md + +PIDE protocol extensions depend on system option "vscode_pide_extensions". +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{PrintStream, OutputStream, File => JFile} + +import scala.annotation.tailrec +import scala.collection.mutable + + +object Language_Server +{ + type Editor = isabelle.Editor[Unit] + + + /* Isabelle tool wrapper */ + + private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") + + val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => + { + try { + var logic_ancestor: Option[String] = None + var log_file: Option[Path] = None + var logic_requirements = false + var dirs: List[Path] = Nil + var include_sessions: List[String] = Nil + var logic = default_logic + var modes: List[String] = Nil + var options = Options.init() + var verbose = false + + val getopts = Getopts(""" +Usage: isabelle vscode_server [OPTIONS] + + Options are: + -A NAME ancestor session for option -R (default: parent) + -L FILE logging on FILE + -R NAME build image with requirements from other sessions + -d DIR include session directory + -i NAME include session in name-space of theories + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) + -m MODE add print mode for output + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v verbose logging + + Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. +""", + "A:" -> (arg => logic_ancestor = Some(arg)), + "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), + "R:" -> (arg => { logic = arg; logic_requirements = true }), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), + "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose = true)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val log = Logger.make(log_file) + val channel = new Channel(System.in, System.out, log, verbose) + val server = + new Language_Server(channel, options, session_name = logic, session_dirs = dirs, + include_sessions = include_sessions, session_ancestor = logic_ancestor, + session_requirements = logic_requirements, modes = modes, log = log) + + // prevent spurious garbage on the main protocol channel + val orig_out = System.out + try { + System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) + server.start() + } + finally { System.setOut(orig_out) } + } + catch { + case exn: Throwable => + val channel = new Channel(System.in, System.out, No_Logger) + channel.error_message(Exn.message(exn)) + throw(exn) + } + }) +} + +class Language_Server( + val channel: Channel, + options: Options, + session_name: String = Language_Server.default_logic, + session_dirs: List[Path] = Nil, + include_sessions: List[String] = Nil, + session_ancestor: Option[String] = None, + session_requirements: Boolean = false, + modes: List[String] = Nil, + log: Logger = No_Logger) +{ + server => + + + /* prover session */ + + private val session_ = Synchronized(None: Option[Session]) + def session: Session = session_.value getOrElse error("Server inactive") + def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] + + def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = + for { + model <- resources.get_model(new JFile(node_pos.name)) + rendering = model.rendering() + offset <- model.content.doc.offset(node_pos.pos) + } yield (rendering, offset) + + private val dynamic_output = Dynamic_Output(server) + + + /* input from client or file-system */ + + private val delay_input: Delay = + Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) + { resources.flush_input(session, channel) } + + private val delay_load: Delay = + Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { + val (invoke_input, invoke_load) = + resources.resolve_dependencies(session, editor, file_watcher) + if (invoke_input) delay_input.invoke() + if (invoke_load) delay_load.invoke + } + + private val file_watcher = + File_Watcher(sync_documents, options.seconds("vscode_load_delay")) + + private def close_document(file: JFile) + { + if (resources.close_model(file)) { + file_watcher.register_parent(file) + sync_documents(Set(file)) + delay_input.invoke() + delay_output.invoke() + } + } + + private def sync_documents(changed: Set[JFile]) + { + resources.sync_models(changed) + delay_input.invoke() + delay_output.invoke() + } + + private def change_document(file: JFile, version: Long, changes: List[LSP.TextDocumentChange]) + { + val norm_changes = new mutable.ListBuffer[LSP.TextDocumentChange] + @tailrec def norm(chs: List[LSP.TextDocumentChange]) + { + if (chs.nonEmpty) { + val (full_texts, rest1) = chs.span(_.range.isEmpty) + val (edits, rest2) = rest1.span(_.range.nonEmpty) + norm_changes ++= full_texts + norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse + norm(rest2) + } + } + norm(changes) + norm_changes.foreach(change => + resources.change_model(session, editor, file, version, change.text, change.range)) + + delay_input.invoke() + delay_output.invoke() + } + + + /* caret handling */ + + private val delay_caret_update: Delay = + Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) + { session.caret_focus.post(Session.Caret_Focus) } + + private def update_caret(caret: Option[(JFile, Line.Position)]) + { + resources.update_caret(caret) + delay_caret_update.invoke() + delay_input.invoke() + } + + + /* preview */ + + private lazy val preview_panel = new Preview_Panel(resources) + + private lazy val delay_preview: Delay = + Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) + { + if (preview_panel.flush(channel)) delay_preview.invoke() + } + + private def request_preview(file: JFile, column: Int) + { + preview_panel.request(file, column) + delay_preview.invoke() + } + + + /* output to client */ + + private val delay_output: Delay = + Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) + { + if (resources.flush_output(channel)) delay_output.invoke() + } + + def update_output(changed_nodes: Traversable[JFile]) + { + resources.update_output(changed_nodes) + delay_output.invoke() + } + + def update_output_visible() + { + resources.update_output_visible() + delay_output.invoke() + } + + private val prover_output = + Session.Consumer[Session.Commands_Changed](getClass.getName) { + case changed => + update_output(changed.nodes.toList.map(resources.node_file(_))) + } + + private val syslog_messages = + Session.Consumer[Prover.Output](getClass.getName) { + case output => channel.log_writeln(resources.output_xml(output.message)) + } + + + /* init and exit */ + + def init(id: LSP.Id) + { + def reply_ok(msg: String) + { + channel.write(LSP.Initialize.reply(id, "")) + channel.writeln(msg) + } + + def reply_error(msg: String) + { + channel.write(LSP.Initialize.reply(id, msg)) + channel.error_message(msg) + } + + val try_session = + try { + val base_info = + Sessions.base_info( + options, session_name, dirs = session_dirs, include_sessions = include_sessions, + session_ancestor = session_ancestor, session_requirements = session_requirements).check + + def build(no_build: Boolean = false): Build.Results = + Build.build(options, + selection = Sessions.Selection.session(base_info.session), + build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) + + if (!build(no_build = true).ok) { + val start_msg = "Build started for Isabelle/" + base_info.session + " ..." + val fail_msg = "Session build failed -- prover process remains inactive!" + + val progress = channel.progress(verbose = true) + progress.echo(start_msg); channel.writeln(start_msg) + + if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } + } + + val resources = new VSCode_Resources(options, base_info, log) + { + override def commit(change: Session.Change): Unit = + if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) + delay_load.invoke() + } + + val session_options = options.bool("editor_output_state") = true + val session = new Session(session_options, resources) + + Some((base_info, session)) + } + catch { case ERROR(msg) => reply_error(msg); None } + + for ((base_info, session) <- try_session) { + session_.change(_ => Some(session)) + + session.commands_changed += prover_output + session.syslog_messages += syslog_messages + + dynamic_output.init() + + try { + Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), + modes = modes, logic = base_info.session).await_startup + reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") + } + catch { case ERROR(msg) => reply_error(msg) } + } + } + + def shutdown(id: LSP.Id) + { + def reply(err: String): Unit = channel.write(LSP.Shutdown.reply(id, err)) + + session_.change({ + case Some(session) => + session.commands_changed -= prover_output + session.syslog_messages -= syslog_messages + + dynamic_output.exit() + + delay_load.revoke() + file_watcher.shutdown() + delay_input.revoke() + delay_output.revoke() + delay_caret_update.revoke() + delay_preview.revoke() + + val result = session.stop() + if (result.ok) reply("") + else reply("Prover shutdown failed: " + result.rc) + None + case None => + reply("Prover inactive") + None + }) + } + + def exit() { + log("\n") + sys.exit(if (session_.value.isDefined) 2 else 0) + } + + + /* completion */ + + def completion(id: LSP.Id, node_pos: Line.Node_Position) + { + val result = + (for ((rendering, offset) <- rendering_offset(node_pos)) + yield rendering.completion(node_pos.pos, offset)) getOrElse Nil + channel.write(LSP.Completion.reply(id, result)) + } + + + /* spell-checker dictionary */ + + def update_dictionary(include: Boolean, permanent: Boolean) + { + for { + spell_checker <- resources.spell_checker.get + caret <- resources.get_caret() + rendering = caret.model.rendering() + range = rendering.before_caret_range(caret.offset) + Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) + } { + spell_checker.update(word, include, permanent) + update_output_visible() + } + } + + def reset_dictionary() + { + for (spell_checker <- resources.spell_checker.get) + { + spell_checker.reset() + update_output_visible() + } + } + + + /* hover */ + + def hover(id: LSP.Id, node_pos: Line.Node_Position) + { + val result = + for { + (rendering, offset) <- rendering_offset(node_pos) + info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) + } yield { + val range = rendering.model.content.doc.range(info.range) + val contents = info.info.map(t => LSP.MarkedString(resources.output_pretty_tooltip(List(t)))) + (range, contents) + } + channel.write(LSP.Hover.reply(id, result)) + } + + + /* goto definition */ + + def goto_definition(id: LSP.Id, node_pos: Line.Node_Position) + { + val result = + (for ((rendering, offset) <- rendering_offset(node_pos)) + yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil + channel.write(LSP.GotoDefinition.reply(id, result)) + } + + + /* document highlights */ + + def document_highlights(id: LSP.Id, node_pos: Line.Node_Position) + { + val result = + (for ((rendering, offset) <- rendering_offset(node_pos)) + yield { + val model = rendering.model + rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) + .map(r => LSP.DocumentHighlight.text(model.content.doc.range(r))) + }) getOrElse Nil + channel.write(LSP.DocumentHighlights.reply(id, result)) + } + + + /* main loop */ + + def start() + { + log("Server started " + Date.now()) + + def handle(json: JSON.T) + { + try { + json match { + case LSP.Initialize(id) => init(id) + case LSP.Initialized(()) => + case LSP.Shutdown(id) => shutdown(id) + case LSP.Exit(()) => exit() + case LSP.DidOpenTextDocument(file, _, version, text) => + change_document(file, version, List(LSP.TextDocumentChange(None, text))) + delay_load.invoke() + case LSP.DidChangeTextDocument(file, version, changes) => + change_document(file, version, changes) + case LSP.DidCloseTextDocument(file) => close_document(file) + case LSP.Completion(id, node_pos) => completion(id, node_pos) + case LSP.Include_Word(()) => update_dictionary(true, false) + case LSP.Include_Word_Permanently(()) => update_dictionary(true, true) + case LSP.Exclude_Word(()) => update_dictionary(false, false) + case LSP.Exclude_Word_Permanently(()) => update_dictionary(false, true) + case LSP.Reset_Words(()) => reset_dictionary() + case LSP.Hover(id, node_pos) => hover(id, node_pos) + case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) + case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) + case LSP.Caret_Update(caret) => update_caret(caret) + case LSP.State_Init(()) => State_Panel.init(server) + case LSP.State_Exit(id) => State_Panel.exit(id) + case LSP.State_Locate(id) => State_Panel.locate(id) + case LSP.State_Update(id) => State_Panel.update(id) + case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) + case LSP.Preview_Request(file, column) => request_preview(file, column) + case LSP.Symbols_Request(()) => channel.write(LSP.Symbols()) + case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED") + } + } + catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } + } + + @tailrec def loop() + { + channel.read() match { + case Some(json) => + json match { + case bulk: List[_] => bulk.foreach(handle) + case _ => handle(json) + } + loop() + case None => log("### TERMINATE") + } + } + loop() + } + + + /* abstract editor operations */ + + object editor extends Language_Server.Editor + { + /* session */ + + override def session: Session = server.session + override def flush(): Unit = resources.flush_input(session, channel) + override def invoke(): Unit = delay_input.invoke() + + + /* current situation */ + + override def current_node(context: Unit): Option[Document.Node.Name] = + resources.get_caret().map(_.model.node_name) + override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = + resources.get_caret().map(_.model.snapshot()) + + override def node_snapshot(name: Document.Node.Name): Document.Snapshot = + { + resources.get_model(name) match { + case Some(model) => model.snapshot() + case None => session.snapshot(name) + } + } + + def current_command(snapshot: Document.Snapshot): Option[Command] = + { + resources.get_caret() match { + case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) + case None => None + } + } + override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = + current_command(snapshot) + + + /* overlays */ + + override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + resources.node_overlays(name) + + override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + resources.insert_overlay(command, fn, args) + + override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + resources.remove_overlay(command, fn, args) + + + /* hyperlinks */ + + override def hyperlink_command( + focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, + offset: Symbol.Offset = 0): Option[Hyperlink] = + { + if (snapshot.is_outdated) None + else + snapshot.find_command_position(id, offset).map(node_pos => + new Hyperlink { + def follow(unit: Unit) { channel.write(LSP.Caret_Update(node_pos, focus)) } + }) + } + + + /* dispatcher thread */ + + override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) + override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) + override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) + override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) + } +} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/lsp.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/lsp.scala Sat Nov 28 20:14:46 2020 +0100 @@ -0,0 +1,626 @@ +/* Title: Tools/VSCode/src/lsp.scala + Author: Makarius + +Message formats for Language Server Protocol 3.0, see +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{File => JFile} + + +object LSP +{ + /* abstract message */ + + object Message + { + val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0") + + def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean) + { + val header = + json match { + case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id") + case _ => JSON.Object.empty + } + if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json)) + else logger(prefix + " " + JSON.Format(header)) + } + } + + + /* notification */ + + object Notification + { + def apply(method: String, params: JSON.T): JSON.T = + Message.empty + ("method" -> method) + ("params" -> params) + + def unapply(json: JSON.T): Option[(String, Option[JSON.T])] = + for { + method <- JSON.string(json, "method") + params = JSON.value(json, "params") + } yield (method, params) + } + + class Notification0(name: String) + { + def unapply(json: JSON.T): Option[Unit] = + json match { + case Notification(method, _) if method == name => Some(()) + case _ => None + } + } + + + /* request message */ + + object Id + { + def empty: Id = Id("") + } + + sealed case class Id(id: Any) + { + require( + id.isInstanceOf[Int] || + id.isInstanceOf[Long] || + id.isInstanceOf[Double] || + id.isInstanceOf[String]) + + override def toString: String = id.toString + } + + object RequestMessage + { + def apply(id: Id, method: String, params: JSON.T): JSON.T = + Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params) + + def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] = + for { + id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id") + method <- JSON.string(json, "method") + params = JSON.value(json, "params") + } yield (Id(id), method, params) + } + + class Request0(name: String) + { + def unapply(json: JSON.T): Option[Id] = + json match { + case RequestMessage(id, method, _) if method == name => Some(id) + case _ => None + } + } + + class RequestTextDocumentPosition(name: String) + { + def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] = + json match { + case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name => + Some((id, node_pos)) + case _ => None + } + } + + + /* response message */ + + object ResponseMessage + { + def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T = + Message.empty + ("id" -> id.id) ++ + JSON.optional("result" -> result) ++ + JSON.optional("error" -> error.map(_.json)) + + def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T = + if (error == "") apply(id, result = result) + else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error))) + + def is_empty(json: JSON.T): Boolean = + JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined + } + + sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) + { + def json: JSON.T = + JSON.Object("code" -> code, "message" -> message) ++ JSON.optional("data" -> data) + } + + object ErrorCodes + { + val ParseError = -32700 + val InvalidRequest = -32600 + val MethodNotFound = -32601 + val InvalidParams = -32602 + val InternalError = -32603 + val serverErrorStart = -32099 + val serverErrorEnd = -32000 + } + + + /* init and exit */ + + object Initialize extends Request0("initialize") + { + def reply(id: Id, error: String): JSON.T = + ResponseMessage.strict( + id, Some(JSON.Object("capabilities" -> ServerCapabilities.json)), error) + } + + object ServerCapabilities + { + val json: JSON.T = + JSON.Object( + "textDocumentSync" -> 2, + "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil), + "hoverProvider" -> true, + "definitionProvider" -> true, + "documentHighlightProvider" -> true) + } + + object Initialized extends Notification0("initialized") + + object Shutdown extends Request0("shutdown") + { + def reply(id: Id, error: String): JSON.T = + ResponseMessage.strict(id, Some("OK"), error) + } + + object Exit extends Notification0("exit") + + + /* document positions */ + + object Position + { + def apply(pos: Line.Position): JSON.T = + JSON.Object("line" -> pos.line, "character" -> pos.column) + + def unapply(json: JSON.T): Option[Line.Position] = + for { + line <- JSON.int(json, "line") + column <- JSON.int(json, "character") + } yield Line.Position(line, column) + } + + object Range + { + def compact(range: Line.Range): List[Int] = + List(range.start.line, range.start.column, range.stop.line, range.stop.column) + + def apply(range: Line.Range): JSON.T = + JSON.Object("start" -> Position(range.start), "end" -> Position(range.stop)) + + def unapply(json: JSON.T): Option[Line.Range] = + (JSON.value(json, "start"), JSON.value(json, "end")) match { + case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop)) + case _ => None + } + } + + object Location + { + def apply(loc: Line.Node_Range): JSON.T = + JSON.Object("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range)) + + def unapply(json: JSON.T): Option[Line.Node_Range] = + for { + uri <- JSON.string(json, "uri") + range_json <- JSON.value(json, "range") + range <- Range.unapply(range_json) + } yield Line.Node_Range(Url.absolute_file_name(uri), range) + } + + object TextDocumentPosition + { + def unapply(json: JSON.T): Option[Line.Node_Position] = + for { + doc <- JSON.value(json, "textDocument") + uri <- JSON.string(doc, "uri") + pos_json <- JSON.value(json, "position") + pos <- Position.unapply(pos_json) + } yield Line.Node_Position(Url.absolute_file_name(uri), pos) + } + + + /* marked strings */ + + sealed case class MarkedString(text: String, language: String = "plaintext") + { + def json: JSON.T = JSON.Object("language" -> language, "value" -> text) + } + + object MarkedStrings + { + def json(msgs: List[MarkedString]): Option[JSON.T] = + msgs match { + case Nil => None + case List(msg) => Some(msg.json) + case _ => Some(msgs.map(_.json)) + } + } + + + /* diagnostic messages */ + + object MessageType + { + val Error = 1 + val Warning = 2 + val Info = 3 + val Log = 4 + } + + object DisplayMessage + { + def apply(message_type: Int, message: String, show: Boolean = true): JSON.T = + Notification(if (show) "window/showMessage" else "window/logMessage", + JSON.Object("type" -> message_type, "message" -> message)) + } + + + /* commands */ + + sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) + { + def json: JSON.T = + JSON.Object("title" -> title, "command" -> command, "arguments" -> arguments) + } + + + /* document edits */ + + object DidOpenTextDocument + { + def unapply(json: JSON.T): Option[(JFile, String, Long, String)] = + json match { + case Notification("textDocument/didOpen", Some(params)) => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + lang <- JSON.string(doc, "languageId") + version <- JSON.long(doc, "version") + text <- JSON.string(doc, "text") + } yield (Url.absolute_file(uri), lang, version, text) + case _ => None + } + } + + + sealed case class TextDocumentChange(range: Option[Line.Range], text: String) + + object DidChangeTextDocument + { + def unapply_change(json: JSON.T): Option[TextDocumentChange] = + for { text <- JSON.string(json, "text") } + yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text) + + def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] = + json match { + case Notification("textDocument/didChange", Some(params)) => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + version <- JSON.long(doc, "version") + changes <- JSON.list(params, "contentChanges", unapply_change _) + } yield (Url.absolute_file(uri), version, changes) + case _ => None + } + } + + class TextDocumentNotification(name: String) + { + def unapply(json: JSON.T): Option[JFile] = + json match { + case Notification(method, Some(params)) if method == name => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + } yield Url.absolute_file(uri) + case _ => None + } + } + + object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose") + object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") + + + /* workspace edits */ + + sealed case class TextEdit(range: Line.Range, new_text: String) + { + def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text) + } + + sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) + { + def json: JSON.T = + JSON.Object( + "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version), + "edits" -> edits.map(_.json)) + } + + object WorkspaceEdit + { + def apply(edits: List[TextDocumentEdit]): JSON.T = + RequestMessage(Id.empty, "workspace/applyEdit", + JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json)))) + } + + + /* completion */ + + sealed case class CompletionItem( + label: String, + kind: Option[Int] = None, + detail: Option[String] = None, + documentation: Option[String] = None, + text: Option[String] = None, + range: Option[Line.Range] = None, + command: Option[Command] = None) + { + def json: JSON.T = + JSON.Object("label" -> label) ++ + JSON.optional("kind" -> kind) ++ + JSON.optional("detail" -> detail) ++ + JSON.optional("documentation" -> documentation) ++ + JSON.optional("insertText" -> text) ++ + JSON.optional("range" -> range.map(Range(_))) ++ + JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++ + JSON.optional("command" -> command.map(_.json)) + } + + object Completion extends RequestTextDocumentPosition("textDocument/completion") + { + def reply(id: Id, result: List[CompletionItem]): JSON.T = + ResponseMessage(id, Some(result.map(_.json))) + } + + + /* spell checker */ + + object Include_Word extends Notification0("PIDE/include_word") + { + val command = Command("Include word", "isabelle.include-word") + } + + object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") + { + val command = Command("Include word permanently", "isabelle.include-word-permanently") + } + + object Exclude_Word extends Notification0("PIDE/exclude_word") + { + val command = Command("Exclude word", "isabelle.exclude-word") + } + + object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") + { + val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently") + } + + object Reset_Words extends Notification0("PIDE/reset_words") + { + val command = Command("Reset non-permanent words", "isabelle.reset-words") + } + + + /* hover request */ + + object Hover extends RequestTextDocumentPosition("textDocument/hover") + { + def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T = + { + val res = + result match { + case Some((range, contents)) => + JSON.Object( + "contents" -> MarkedStrings.json(contents).getOrElse(Nil), + "range" -> Range(range)) + case None => JSON.Object("contents" -> Nil) + } + ResponseMessage(id, Some(res)) + } + } + + + /* goto definition request */ + + object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") + { + def reply(id: Id, result: List[Line.Node_Range]): JSON.T = + ResponseMessage(id, Some(result.map(Location.apply(_)))) + } + + + /* document highlights request */ + + object DocumentHighlight + { + def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1)) + def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2)) + def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3)) + } + + sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) + { + def json: JSON.T = + kind match { + case None => JSON.Object("range" -> Range(range)) + case Some(k) => JSON.Object("range" -> Range(range), "kind" -> k) + } + } + + object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") + { + def reply(id: Id, result: List[DocumentHighlight]): JSON.T = + ResponseMessage(id, Some(result.map(_.json))) + } + + + /* diagnostics */ + + sealed case class Diagnostic(range: Line.Range, message: String, + severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None) + { + def json: JSON.T = + Message.empty + ("range" -> Range(range)) + ("message" -> message) ++ + JSON.optional("severity" -> severity) ++ + JSON.optional("code" -> code) ++ + JSON.optional("source" -> source) + } + + object DiagnosticSeverity + { + val Error = 1 + val Warning = 2 + val Information = 3 + val Hint = 4 + } + + object PublishDiagnostics + { + def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T = + Notification("textDocument/publishDiagnostics", + JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json))) + } + + + /* decorations */ + + sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString]) + { + def json: JSON.T = + JSON.Object("range" -> Range.compact(range)) ++ + JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) + } + + sealed case class Decoration(typ: String, content: List[DecorationOpts]) + { + def json(file: JFile): JSON.T = + Notification("PIDE/decoration", + JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) + } + + + /* caret update: bidirectional */ + + object Caret_Update + { + def apply(node_pos: Line.Node_Position, focus: Boolean): JSON.T = + Notification("PIDE/caret_update", + JSON.Object( + "uri" -> Url.print_file_name(node_pos.name), + "line" -> node_pos.pos.line, + "character" -> node_pos.pos.column, + "focus" -> focus)) + + def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] = + json match { + case Notification("PIDE/caret_update", Some(params)) => + val caret = + for { + uri <- JSON.string(params, "uri") + if Url.is_wellformed_file(uri) + pos <- Position.unapply(params) + } yield (Url.absolute_file(uri), pos) + Some(caret) + case _ => None + } + } + + + /* dynamic output */ + + object Dynamic_Output + { + def apply(content: String): JSON.T = + Notification("PIDE/dynamic_output", JSON.Object("content" -> content)) + } + + + /* state output */ + + object State_Output + { + def apply(id: Counter.ID, content: String): JSON.T = + Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content)) + } + + class State_Id_Notification(name: String) + { + def unapply(json: JSON.T): Option[Counter.ID] = + json match { + case Notification(method, Some(params)) if method == name => JSON.long(params, "id") + case _ => None + } + } + + object State_Init extends Notification0("PIDE/state_init") + object State_Exit extends State_Id_Notification("PIDE/state_exit") + object State_Locate extends State_Id_Notification("PIDE/state_locate") + object State_Update extends State_Id_Notification("PIDE/state_update") + + object State_Auto_Update + { + def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] = + json match { + case Notification("PIDE/state_auto_update", Some(params)) => + for { + id <- JSON.long(params, "id") + enabled <- JSON.bool(params, "enabled") + } yield (id, enabled) + case _ => None + } + } + + + /* preview */ + + object Preview_Request + { + def unapply(json: JSON.T): Option[(JFile, Int)] = + json match { + case Notification("PIDE/preview_request", Some(params)) => + for { + uri <- JSON.string(params, "uri") + if Url.is_wellformed_file(uri) + column <- JSON.int(params, "column") + } yield (Url.absolute_file(uri), column) + case _ => None + } + } + + object Preview_Response + { + def apply(file: JFile, column: Int, label: String, content: String): JSON.T = + Notification("PIDE/preview_response", + JSON.Object( + "uri" -> Url.print_file(file), + "column" -> column, + "label" -> label, + "content" -> content)) + } + + + /* Isabelle symbols */ + + object Symbols_Request extends Notification0("PIDE/symbols_request") + + object Symbols + { + def apply(): JSON.T = + { + val entries = + for ((sym, code) <- Symbol.codes) + yield JSON.Object("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code) + Notification("PIDE/symbols", JSON.Object("entries" -> entries)) + } + } +} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/preview_panel.scala Sat Nov 28 20:14:46 2020 +0100 @@ -31,8 +31,7 @@ if (snapshot.is_outdated) m else { val preview = Presentation.preview(resources, snapshot) - channel.write( - Protocol.Preview_Response(file, column, preview.title, preview.content)) + channel.write(LSP.Preview_Response(file, column, preview.title, preview.content)) m - file } case None => m - file diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Sat Nov 28 17:38:03 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,626 +0,0 @@ -/* Title: Tools/VSCode/src/protocol.scala - Author: Makarius - -Message formats for Language Server Protocol 3.0, see -https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md -*/ - -package isabelle.vscode - - -import isabelle._ - -import java.io.{File => JFile} - - -object Protocol -{ - /* abstract message */ - - object Message - { - val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0") - - def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean) - { - val header = - json match { - case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id") - case _ => JSON.Object.empty - } - if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json)) - else logger(prefix + " " + JSON.Format(header)) - } - } - - - /* notification */ - - object Notification - { - def apply(method: String, params: JSON.T): JSON.T = - Message.empty + ("method" -> method) + ("params" -> params) - - def unapply(json: JSON.T): Option[(String, Option[JSON.T])] = - for { - method <- JSON.string(json, "method") - params = JSON.value(json, "params") - } yield (method, params) - } - - class Notification0(name: String) - { - def unapply(json: JSON.T): Option[Unit] = - json match { - case Notification(method, _) if method == name => Some(()) - case _ => None - } - } - - - /* request message */ - - object Id - { - def empty: Id = Id("") - } - - sealed case class Id(id: Any) - { - require( - id.isInstanceOf[Int] || - id.isInstanceOf[Long] || - id.isInstanceOf[Double] || - id.isInstanceOf[String]) - - override def toString: String = id.toString - } - - object RequestMessage - { - def apply(id: Id, method: String, params: JSON.T): JSON.T = - Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params) - - def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] = - for { - id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id") - method <- JSON.string(json, "method") - params = JSON.value(json, "params") - } yield (Id(id), method, params) - } - - class Request0(name: String) - { - def unapply(json: JSON.T): Option[Id] = - json match { - case RequestMessage(id, method, _) if method == name => Some(id) - case _ => None - } - } - - class RequestTextDocumentPosition(name: String) - { - def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] = - json match { - case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name => - Some((id, node_pos)) - case _ => None - } - } - - - /* response message */ - - object ResponseMessage - { - def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T = - Message.empty + ("id" -> id.id) ++ - JSON.optional("result" -> result) ++ - JSON.optional("error" -> error.map(_.json)) - - def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T = - if (error == "") apply(id, result = result) - else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error))) - - def is_empty(json: JSON.T): Boolean = - JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined - } - - sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) - { - def json: JSON.T = - JSON.Object("code" -> code, "message" -> message) ++ JSON.optional("data" -> data) - } - - object ErrorCodes - { - val ParseError = -32700 - val InvalidRequest = -32600 - val MethodNotFound = -32601 - val InvalidParams = -32602 - val InternalError = -32603 - val serverErrorStart = -32099 - val serverErrorEnd = -32000 - } - - - /* init and exit */ - - object Initialize extends Request0("initialize") - { - def reply(id: Id, error: String): JSON.T = - ResponseMessage.strict( - id, Some(JSON.Object("capabilities" -> ServerCapabilities.json)), error) - } - - object ServerCapabilities - { - val json: JSON.T = - JSON.Object( - "textDocumentSync" -> 2, - "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil), - "hoverProvider" -> true, - "definitionProvider" -> true, - "documentHighlightProvider" -> true) - } - - object Initialized extends Notification0("initialized") - - object Shutdown extends Request0("shutdown") - { - def reply(id: Id, error: String): JSON.T = - ResponseMessage.strict(id, Some("OK"), error) - } - - object Exit extends Notification0("exit") - - - /* document positions */ - - object Position - { - def apply(pos: Line.Position): JSON.T = - JSON.Object("line" -> pos.line, "character" -> pos.column) - - def unapply(json: JSON.T): Option[Line.Position] = - for { - line <- JSON.int(json, "line") - column <- JSON.int(json, "character") - } yield Line.Position(line, column) - } - - object Range - { - def compact(range: Line.Range): List[Int] = - List(range.start.line, range.start.column, range.stop.line, range.stop.column) - - def apply(range: Line.Range): JSON.T = - JSON.Object("start" -> Position(range.start), "end" -> Position(range.stop)) - - def unapply(json: JSON.T): Option[Line.Range] = - (JSON.value(json, "start"), JSON.value(json, "end")) match { - case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop)) - case _ => None - } - } - - object Location - { - def apply(loc: Line.Node_Range): JSON.T = - JSON.Object("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range)) - - def unapply(json: JSON.T): Option[Line.Node_Range] = - for { - uri <- JSON.string(json, "uri") - range_json <- JSON.value(json, "range") - range <- Range.unapply(range_json) - } yield Line.Node_Range(Url.absolute_file_name(uri), range) - } - - object TextDocumentPosition - { - def unapply(json: JSON.T): Option[Line.Node_Position] = - for { - doc <- JSON.value(json, "textDocument") - uri <- JSON.string(doc, "uri") - pos_json <- JSON.value(json, "position") - pos <- Position.unapply(pos_json) - } yield Line.Node_Position(Url.absolute_file_name(uri), pos) - } - - - /* marked strings */ - - sealed case class MarkedString(text: String, language: String = "plaintext") - { - def json: JSON.T = JSON.Object("language" -> language, "value" -> text) - } - - object MarkedStrings - { - def json(msgs: List[MarkedString]): Option[JSON.T] = - msgs match { - case Nil => None - case List(msg) => Some(msg.json) - case _ => Some(msgs.map(_.json)) - } - } - - - /* diagnostic messages */ - - object MessageType - { - val Error = 1 - val Warning = 2 - val Info = 3 - val Log = 4 - } - - object DisplayMessage - { - def apply(message_type: Int, message: String, show: Boolean = true): JSON.T = - Notification(if (show) "window/showMessage" else "window/logMessage", - JSON.Object("type" -> message_type, "message" -> message)) - } - - - /* commands */ - - sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) - { - def json: JSON.T = - JSON.Object("title" -> title, "command" -> command, "arguments" -> arguments) - } - - - /* document edits */ - - object DidOpenTextDocument - { - def unapply(json: JSON.T): Option[(JFile, String, Long, String)] = - json match { - case Notification("textDocument/didOpen", Some(params)) => - for { - doc <- JSON.value(params, "textDocument") - uri <- JSON.string(doc, "uri") - lang <- JSON.string(doc, "languageId") - version <- JSON.long(doc, "version") - text <- JSON.string(doc, "text") - } yield (Url.absolute_file(uri), lang, version, text) - case _ => None - } - } - - - sealed case class TextDocumentChange(range: Option[Line.Range], text: String) - - object DidChangeTextDocument - { - def unapply_change(json: JSON.T): Option[TextDocumentChange] = - for { text <- JSON.string(json, "text") } - yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text) - - def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] = - json match { - case Notification("textDocument/didChange", Some(params)) => - for { - doc <- JSON.value(params, "textDocument") - uri <- JSON.string(doc, "uri") - version <- JSON.long(doc, "version") - changes <- JSON.list(params, "contentChanges", unapply_change _) - } yield (Url.absolute_file(uri), version, changes) - case _ => None - } - } - - class TextDocumentNotification(name: String) - { - def unapply(json: JSON.T): Option[JFile] = - json match { - case Notification(method, Some(params)) if method == name => - for { - doc <- JSON.value(params, "textDocument") - uri <- JSON.string(doc, "uri") - } yield Url.absolute_file(uri) - case _ => None - } - } - - object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose") - object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") - - - /* workspace edits */ - - sealed case class TextEdit(range: Line.Range, new_text: String) - { - def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text) - } - - sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) - { - def json: JSON.T = - JSON.Object( - "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version), - "edits" -> edits.map(_.json)) - } - - object WorkspaceEdit - { - def apply(edits: List[TextDocumentEdit]): JSON.T = - RequestMessage(Id.empty, "workspace/applyEdit", - JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json)))) - } - - - /* completion */ - - sealed case class CompletionItem( - label: String, - kind: Option[Int] = None, - detail: Option[String] = None, - documentation: Option[String] = None, - text: Option[String] = None, - range: Option[Line.Range] = None, - command: Option[Command] = None) - { - def json: JSON.T = - JSON.Object("label" -> label) ++ - JSON.optional("kind" -> kind) ++ - JSON.optional("detail" -> detail) ++ - JSON.optional("documentation" -> documentation) ++ - JSON.optional("insertText" -> text) ++ - JSON.optional("range" -> range.map(Range(_))) ++ - JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++ - JSON.optional("command" -> command.map(_.json)) - } - - object Completion extends RequestTextDocumentPosition("textDocument/completion") - { - def reply(id: Id, result: List[CompletionItem]): JSON.T = - ResponseMessage(id, Some(result.map(_.json))) - } - - - /* spell checker */ - - object Include_Word extends Notification0("PIDE/include_word") - { - val command = Command("Include word", "isabelle.include-word") - } - - object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") - { - val command = Command("Include word permanently", "isabelle.include-word-permanently") - } - - object Exclude_Word extends Notification0("PIDE/exclude_word") - { - val command = Command("Exclude word", "isabelle.exclude-word") - } - - object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") - { - val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently") - } - - object Reset_Words extends Notification0("PIDE/reset_words") - { - val command = Command("Reset non-permanent words", "isabelle.reset-words") - } - - - /* hover request */ - - object Hover extends RequestTextDocumentPosition("textDocument/hover") - { - def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T = - { - val res = - result match { - case Some((range, contents)) => - JSON.Object( - "contents" -> MarkedStrings.json(contents).getOrElse(Nil), - "range" -> Range(range)) - case None => JSON.Object("contents" -> Nil) - } - ResponseMessage(id, Some(res)) - } - } - - - /* goto definition request */ - - object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") - { - def reply(id: Id, result: List[Line.Node_Range]): JSON.T = - ResponseMessage(id, Some(result.map(Location.apply(_)))) - } - - - /* document highlights request */ - - object DocumentHighlight - { - def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1)) - def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2)) - def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3)) - } - - sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) - { - def json: JSON.T = - kind match { - case None => JSON.Object("range" -> Range(range)) - case Some(k) => JSON.Object("range" -> Range(range), "kind" -> k) - } - } - - object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") - { - def reply(id: Id, result: List[DocumentHighlight]): JSON.T = - ResponseMessage(id, Some(result.map(_.json))) - } - - - /* diagnostics */ - - sealed case class Diagnostic(range: Line.Range, message: String, - severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None) - { - def json: JSON.T = - Message.empty + ("range" -> Range(range)) + ("message" -> message) ++ - JSON.optional("severity" -> severity) ++ - JSON.optional("code" -> code) ++ - JSON.optional("source" -> source) - } - - object DiagnosticSeverity - { - val Error = 1 - val Warning = 2 - val Information = 3 - val Hint = 4 - } - - object PublishDiagnostics - { - def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T = - Notification("textDocument/publishDiagnostics", - JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json))) - } - - - /* decorations */ - - sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString]) - { - def json: JSON.T = - JSON.Object("range" -> Range.compact(range)) ++ - JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) - } - - sealed case class Decoration(typ: String, content: List[DecorationOpts]) - { - def json(file: JFile): JSON.T = - Notification("PIDE/decoration", - JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) - } - - - /* caret update: bidirectional */ - - object Caret_Update - { - def apply(node_pos: Line.Node_Position, focus: Boolean): JSON.T = - Notification("PIDE/caret_update", - JSON.Object( - "uri" -> Url.print_file_name(node_pos.name), - "line" -> node_pos.pos.line, - "character" -> node_pos.pos.column, - "focus" -> focus)) - - def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] = - json match { - case Notification("PIDE/caret_update", Some(params)) => - val caret = - for { - uri <- JSON.string(params, "uri") - if Url.is_wellformed_file(uri) - pos <- Position.unapply(params) - } yield (Url.absolute_file(uri), pos) - Some(caret) - case _ => None - } - } - - - /* dynamic output */ - - object Dynamic_Output - { - def apply(content: String): JSON.T = - Notification("PIDE/dynamic_output", JSON.Object("content" -> content)) - } - - - /* state output */ - - object State_Output - { - def apply(id: Counter.ID, content: String): JSON.T = - Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content)) - } - - class State_Id_Notification(name: String) - { - def unapply(json: JSON.T): Option[Counter.ID] = - json match { - case Notification(method, Some(params)) if method == name => JSON.long(params, "id") - case _ => None - } - } - - object State_Init extends Notification0("PIDE/state_init") - object State_Exit extends State_Id_Notification("PIDE/state_exit") - object State_Locate extends State_Id_Notification("PIDE/state_locate") - object State_Update extends State_Id_Notification("PIDE/state_update") - - object State_Auto_Update - { - def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] = - json match { - case Notification("PIDE/state_auto_update", Some(params)) => - for { - id <- JSON.long(params, "id") - enabled <- JSON.bool(params, "enabled") - } yield (id, enabled) - case _ => None - } - } - - - /* preview */ - - object Preview_Request - { - def unapply(json: JSON.T): Option[(JFile, Int)] = - json match { - case Notification("PIDE/preview_request", Some(params)) => - for { - uri <- JSON.string(params, "uri") - if Url.is_wellformed_file(uri) - column <- JSON.int(params, "column") - } yield (Url.absolute_file(uri), column) - case _ => None - } - } - - object Preview_Response - { - def apply(file: JFile, column: Int, label: String, content: String): JSON.T = - Notification("PIDE/preview_response", - JSON.Object( - "uri" -> Url.print_file(file), - "column" -> column, - "label" -> label, - "content" -> content)) - } - - - /* Isabelle symbols */ - - object Symbols_Request extends Notification0("PIDE/symbols_request") - - object Symbols - { - def apply(): JSON.T = - { - val entries = - for ((sym, code) <- Symbol.codes) - yield JSON.Object("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code) - Notification("PIDE/symbols", JSON.Object("entries" -> entries)) - } - } -} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sat Nov 28 17:38:03 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,560 +0,0 @@ -/* Title: Tools/VSCode/src/server.scala - Author: Makarius - -Server for VS Code Language Server Protocol 2.0/3.0, see also -https://github.com/Microsoft/language-server-protocol -https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md - -PIDE protocol extensions depend on system option "vscode_pide_extensions". -*/ - -package isabelle.vscode - - -import isabelle._ - -import java.io.{PrintStream, OutputStream, File => JFile} - -import scala.annotation.tailrec -import scala.collection.mutable - - -object Server -{ - type Editor = isabelle.Editor[Unit] - - - /* Isabelle tool wrapper */ - - private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") - - val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => - { - try { - var logic_ancestor: Option[String] = None - var log_file: Option[Path] = None - var logic_requirements = false - var dirs: List[Path] = Nil - var include_sessions: List[String] = Nil - var logic = default_logic - var modes: List[String] = Nil - var options = Options.init() - var verbose = false - - val getopts = Getopts(""" -Usage: isabelle vscode_server [OPTIONS] - - Options are: - -A NAME ancestor session for option -R (default: parent) - -L FILE logging on FILE - -R NAME build image with requirements from other sessions - -d DIR include session directory - -i NAME include session in name-space of theories - -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) - -m MODE add print mode for output - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v verbose logging - - Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. -""", - "A:" -> (arg => logic_ancestor = Some(arg)), - "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), - "R:" -> (arg => { logic = arg; logic_requirements = true }), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), - "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), - "l:" -> (arg => logic = arg), - "m:" -> (arg => modes = arg :: modes), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose = true)) - - val more_args = getopts(args) - if (more_args.nonEmpty) getopts.usage() - - val log = Logger.make(log_file) - val channel = new Channel(System.in, System.out, log, verbose) - val server = - new Server(channel, options, session_name = logic, session_dirs = dirs, - include_sessions = include_sessions, session_ancestor = logic_ancestor, - session_requirements = logic_requirements, modes = modes, log = log) - - // prevent spurious garbage on the main protocol channel - val orig_out = System.out - try { - System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) - server.start() - } - finally { System.setOut(orig_out) } - } - catch { - case exn: Throwable => - val channel = new Channel(System.in, System.out, No_Logger) - channel.error_message(Exn.message(exn)) - throw(exn) - } - }) -} - -class Server( - val channel: Channel, - options: Options, - session_name: String = Server.default_logic, - session_dirs: List[Path] = Nil, - include_sessions: List[String] = Nil, - session_ancestor: Option[String] = None, - session_requirements: Boolean = false, - modes: List[String] = Nil, - log: Logger = No_Logger) -{ - server => - - - /* prover session */ - - private val session_ = Synchronized(None: Option[Session]) - def session: Session = session_.value getOrElse error("Server inactive") - def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] - - def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = - for { - model <- resources.get_model(new JFile(node_pos.name)) - rendering = model.rendering() - offset <- model.content.doc.offset(node_pos.pos) - } yield (rendering, offset) - - private val dynamic_output = Dynamic_Output(server) - - - /* input from client or file-system */ - - private val delay_input: Delay = - Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) - { resources.flush_input(session, channel) } - - private val delay_load: Delay = - Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { - val (invoke_input, invoke_load) = - resources.resolve_dependencies(session, editor, file_watcher) - if (invoke_input) delay_input.invoke() - if (invoke_load) delay_load.invoke - } - - private val file_watcher = - File_Watcher(sync_documents, options.seconds("vscode_load_delay")) - - private def close_document(file: JFile) - { - if (resources.close_model(file)) { - file_watcher.register_parent(file) - sync_documents(Set(file)) - delay_input.invoke() - delay_output.invoke() - } - } - - private def sync_documents(changed: Set[JFile]) - { - resources.sync_models(changed) - delay_input.invoke() - delay_output.invoke() - } - - private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange]) - { - val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] - @tailrec def norm(chs: List[Protocol.TextDocumentChange]) - { - if (chs.nonEmpty) { - val (full_texts, rest1) = chs.span(_.range.isEmpty) - val (edits, rest2) = rest1.span(_.range.nonEmpty) - norm_changes ++= full_texts - norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse - norm(rest2) - } - } - norm(changes) - norm_changes.foreach(change => - resources.change_model(session, editor, file, version, change.text, change.range)) - - delay_input.invoke() - delay_output.invoke() - } - - - /* caret handling */ - - private val delay_caret_update: Delay = - Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) - { session.caret_focus.post(Session.Caret_Focus) } - - private def update_caret(caret: Option[(JFile, Line.Position)]) - { - resources.update_caret(caret) - delay_caret_update.invoke() - delay_input.invoke() - } - - - /* preview */ - - private lazy val preview_panel = new Preview_Panel(resources) - - private lazy val delay_preview: Delay = - Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) - { - if (preview_panel.flush(channel)) delay_preview.invoke() - } - - private def request_preview(file: JFile, column: Int) - { - preview_panel.request(file, column) - delay_preview.invoke() - } - - - /* output to client */ - - private val delay_output: Delay = - Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) - { - if (resources.flush_output(channel)) delay_output.invoke() - } - - def update_output(changed_nodes: Traversable[JFile]) - { - resources.update_output(changed_nodes) - delay_output.invoke() - } - - def update_output_visible() - { - resources.update_output_visible() - delay_output.invoke() - } - - private val prover_output = - Session.Consumer[Session.Commands_Changed](getClass.getName) { - case changed => - update_output(changed.nodes.toList.map(resources.node_file(_))) - } - - private val syslog_messages = - Session.Consumer[Prover.Output](getClass.getName) { - case output => channel.log_writeln(resources.output_xml(output.message)) - } - - - /* init and exit */ - - def init(id: Protocol.Id) - { - def reply_ok(msg: String) - { - channel.write(Protocol.Initialize.reply(id, "")) - channel.writeln(msg) - } - - def reply_error(msg: String) - { - channel.write(Protocol.Initialize.reply(id, msg)) - channel.error_message(msg) - } - - val try_session = - try { - val base_info = - Sessions.base_info( - options, session_name, dirs = session_dirs, include_sessions = include_sessions, - session_ancestor = session_ancestor, session_requirements = session_requirements).check - - def build(no_build: Boolean = false): Build.Results = - Build.build(options, - selection = Sessions.Selection.session(base_info.session), - build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) - - if (!build(no_build = true).ok) { - val start_msg = "Build started for Isabelle/" + base_info.session + " ..." - val fail_msg = "Session build failed -- prover process remains inactive!" - - val progress = channel.progress(verbose = true) - progress.echo(start_msg); channel.writeln(start_msg) - - if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } - } - - val resources = new VSCode_Resources(options, base_info, log) - { - override def commit(change: Session.Change): Unit = - if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) - delay_load.invoke() - } - - val session_options = options.bool("editor_output_state") = true - val session = new Session(session_options, resources) - - Some((base_info, session)) - } - catch { case ERROR(msg) => reply_error(msg); None } - - for ((base_info, session) <- try_session) { - session_.change(_ => Some(session)) - - session.commands_changed += prover_output - session.syslog_messages += syslog_messages - - dynamic_output.init() - - try { - Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), - modes = modes, logic = base_info.session).await_startup - reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") - } - catch { case ERROR(msg) => reply_error(msg) } - } - } - - def shutdown(id: Protocol.Id) - { - def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) - - session_.change({ - case Some(session) => - session.commands_changed -= prover_output - session.syslog_messages -= syslog_messages - - dynamic_output.exit() - - delay_load.revoke() - file_watcher.shutdown() - delay_input.revoke() - delay_output.revoke() - delay_caret_update.revoke() - delay_preview.revoke() - - val result = session.stop() - if (result.ok) reply("") - else reply("Prover shutdown failed: " + result.rc) - None - case None => - reply("Prover inactive") - None - }) - } - - def exit() { - log("\n") - sys.exit(if (session_.value.isDefined) 2 else 0) - } - - - /* completion */ - - def completion(id: Protocol.Id, node_pos: Line.Node_Position) - { - val result = - (for ((rendering, offset) <- rendering_offset(node_pos)) - yield rendering.completion(node_pos.pos, offset)) getOrElse Nil - channel.write(Protocol.Completion.reply(id, result)) - } - - - /* spell-checker dictionary */ - - def update_dictionary(include: Boolean, permanent: Boolean) - { - for { - spell_checker <- resources.spell_checker.get - caret <- resources.get_caret() - rendering = caret.model.rendering() - range = rendering.before_caret_range(caret.offset) - Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) - } { - spell_checker.update(word, include, permanent) - update_output_visible() - } - } - - def reset_dictionary() - { - for (spell_checker <- resources.spell_checker.get) - { - spell_checker.reset() - update_output_visible() - } - } - - - /* hover */ - - def hover(id: Protocol.Id, node_pos: Line.Node_Position) - { - val result = - for { - (rendering, offset) <- rendering_offset(node_pos) - info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) - } yield { - val range = rendering.model.content.doc.range(info.range) - val contents = - info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) - (range, contents) - } - channel.write(Protocol.Hover.reply(id, result)) - } - - - /* goto definition */ - - def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) - { - val result = - (for ((rendering, offset) <- rendering_offset(node_pos)) - yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil - channel.write(Protocol.GotoDefinition.reply(id, result)) - } - - - /* document highlights */ - - def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) - { - val result = - (for ((rendering, offset) <- rendering_offset(node_pos)) - yield { - val model = rendering.model - rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) - .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r))) - }) getOrElse Nil - channel.write(Protocol.DocumentHighlights.reply(id, result)) - } - - - /* main loop */ - - def start() - { - log("Server started " + Date.now()) - - def handle(json: JSON.T) - { - try { - json match { - case Protocol.Initialize(id) => init(id) - case Protocol.Initialized(()) => - case Protocol.Shutdown(id) => shutdown(id) - case Protocol.Exit(()) => exit() - case Protocol.DidOpenTextDocument(file, _, version, text) => - change_document(file, version, List(Protocol.TextDocumentChange(None, text))) - delay_load.invoke() - case Protocol.DidChangeTextDocument(file, version, changes) => - change_document(file, version, changes) - case Protocol.DidCloseTextDocument(file) => close_document(file) - case Protocol.Completion(id, node_pos) => completion(id, node_pos) - case Protocol.Include_Word(()) => update_dictionary(true, false) - case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) - case Protocol.Exclude_Word(()) => update_dictionary(false, false) - case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) - case Protocol.Reset_Words(()) => reset_dictionary() - case Protocol.Hover(id, node_pos) => hover(id, node_pos) - case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) - case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) - case Protocol.Caret_Update(caret) => update_caret(caret) - case Protocol.State_Init(()) => State_Panel.init(server) - case Protocol.State_Exit(id) => State_Panel.exit(id) - case Protocol.State_Locate(id) => State_Panel.locate(id) - case Protocol.State_Update(id) => State_Panel.update(id) - case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) - case Protocol.Preview_Request(file, column) => request_preview(file, column) - case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) - case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED") - } - } - catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } - } - - @tailrec def loop() - { - channel.read() match { - case Some(json) => - json match { - case bulk: List[_] => bulk.foreach(handle) - case _ => handle(json) - } - loop() - case None => log("### TERMINATE") - } - } - loop() - } - - - /* abstract editor operations */ - - object editor extends Server.Editor - { - /* session */ - - override def session: Session = server.session - override def flush(): Unit = resources.flush_input(session, channel) - override def invoke(): Unit = delay_input.invoke() - - - /* current situation */ - - override def current_node(context: Unit): Option[Document.Node.Name] = - resources.get_caret().map(_.model.node_name) - override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = - resources.get_caret().map(_.model.snapshot()) - - override def node_snapshot(name: Document.Node.Name): Document.Snapshot = - { - resources.get_model(name) match { - case Some(model) => model.snapshot() - case None => session.snapshot(name) - } - } - - def current_command(snapshot: Document.Snapshot): Option[Command] = - { - resources.get_caret() match { - case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) - case None => None - } - } - override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = - current_command(snapshot) - - - /* overlays */ - - override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = - resources.node_overlays(name) - - override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = - resources.insert_overlay(command, fn, args) - - override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = - resources.remove_overlay(command, fn, args) - - - /* hyperlinks */ - - override def hyperlink_command( - focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, - offset: Symbol.Offset = 0): Option[Hyperlink] = - { - if (snapshot.is_outdated) None - else - snapshot.find_command_position(id, offset).map(node_pos => - new Hyperlink { - def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) } - }) - } - - - /* dispatcher thread */ - - override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) - override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) - override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) - override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) - } -} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/state_panel.scala --- a/src/Tools/VSCode/src/state_panel.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/state_panel.scala Sat Nov 28 20:14:46 2020 +0100 @@ -15,7 +15,7 @@ private val make_id = Counter.make() private val instances = Synchronized(Map.empty[Counter.ID, State_Panel]) - def init(server: Server) + def init(server: Language_Server) { val instance = new State_Panel(server) instances.change(_ + (instance.id -> instance)) @@ -45,14 +45,14 @@ } -class State_Panel private(val server: Server) +class State_Panel private(val server: Language_Server) { /* output */ val id: Counter.ID = State_Panel.make_id() private def output(content: String): Unit = - server.channel.write(Protocol.State_Output(id, content)) + server.channel.write(LSP.State_Output(id, content)) /* query operation */ diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/vscode_model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/vscode_model.scala Sat Nov 28 20:14:46 2020 +0100 @@ -0,0 +1,248 @@ +/* Title: Tools/VSCode/src/vscode_model.scala + Author: Makarius + +VSCode document model for line-oriented text. +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{File => JFile} + + +object VSCode_Model +{ + /* decorations */ + + object Decoration + { + def empty(typ: String): Decoration = Decoration(typ, Nil) + + def ranges(typ: String, ranges: List[Text.Range]): Decoration = + Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) + } + sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) + + + /* content */ + + object Content + { + val empty: Content = Content(Line.Document.empty) + } + + sealed case class Content(doc: Line.Document) + { + override def toString: String = doc.toString + def text_length: Text.Offset = doc.text_length + def text_range: Text.Range = doc.text_range + def text: String = doc.text + + lazy val bytes: Bytes = Bytes(text) + lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) + lazy val bibtex_entries: List[Text.Info[String]] = + try { Bibtex.entries(text) } + catch { case ERROR(_) => Nil } + + def recode_symbols: List[LSP.TextEdit] = + (for { + (line, l) <- doc.lines.iterator.zipWithIndex + text1 = Symbol.encode(line.text) + if (line.text != text1) + } yield { + val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length)) + LSP.TextEdit(range, text1) + }).toList + } + + def init(session: Session, editor: Language_Server.Editor, node_name: Document.Node.Name) + : VSCode_Model = + { + VSCode_Model(session, editor, node_name, Content.empty, + node_required = File_Format.registry.is_theory(node_name)) + } +} + +sealed case class VSCode_Model( + session: Session, + editor: Language_Server.Editor, + node_name: Document.Node.Name, + content: VSCode_Model.Content, + version: Option[Long] = None, + external_file: Boolean = false, + node_required: Boolean = false, + last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, + pending_edits: List[Text.Edit] = Nil, + published_diagnostics: List[Text.Info[Command.Results]] = Nil, + published_decorations: List[VSCode_Model.Decoration] = Nil) extends Document.Model +{ + model => + + + /* content */ + + def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) + + def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version)) + + + /* external file */ + + def external(b: Boolean): VSCode_Model = copy(external_file = b) + + def node_visible: Boolean = !external_file + + + /* header */ + + def node_header: Document.Node.Header = + resources.special_header(node_name) getOrElse + resources.check_thy_reader(node_name, Scan.char_reader(content.text)) + + + /* perspective */ + + def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position]) + : (Boolean, Document.Node.Perspective_Text) = + { + if (is_theory) { + val snapshot = model.snapshot() + + val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 + val caret_range = + if (caret_perspective != 0) { + caret match { + case Some(pos) => + val doc = content.doc + val pos1 = Line.Position((pos.line - caret_perspective) max 0) + val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length) + Text.Range(doc.offset(pos1).get, doc.offset(pos2).get) + case None => Text.Range.offside + } + } + else if (node_visible) content.text_range + else Text.Range.offside + + val text_perspective = + if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) + Text.Perspective.full + else + content.text_range.try_restrict(caret_range) match { + case Some(range) => Text.Perspective(List(range)) + case None => Text.Perspective.empty + } + + val overlays = editor.node_overlays(node_name) + + (snapshot.node.load_commands_changed(doc_blobs), + Document.Node.Perspective(node_required, text_perspective, overlays)) + } + else (false, Document.Node.no_perspective_text) + } + + + /* blob */ + + def get_blob: Option[Document.Blob] = + if (is_theory) None + else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) + + + /* bibtex entries */ + + def bibtex_entries: List[Text.Info[String]] = + model.content.bibtex_entries + + + /* edits */ + + def change_text(text: String, range: Option[Line.Range] = None): Option[VSCode_Model] = + { + val insert = Line.normalize(text) + range match { + case None => + Text.Edit.replace(0, content.text, insert) match { + case Nil => None + case edits => + val content1 = VSCode_Model.Content(Line.Document(insert)) + Some(copy(content = content1, pending_edits = pending_edits ::: edits)) + } + case Some(remove) => + content.doc.change(remove, insert) match { + case None => error("Failed to apply document change: " + remove) + case Some((Nil, _)) => None + case Some((edits, doc1)) => + val content1 = VSCode_Model.Content(doc1) + Some(copy(content = content1, pending_edits = pending_edits ::: edits)) + } + } + } + + def flush_edits( + unicode_symbols: Boolean, + doc_blobs: Document.Blobs, + file: JFile, + caret: Option[Line.Position]) + : Option[((List[LSP.TextDocumentEdit], List[Document.Edit_Text]), VSCode_Model)] = + { + val workspace_edits = + if (unicode_symbols && version.isDefined) { + val edits = content.recode_symbols + if (edits.nonEmpty) List(LSP.TextDocumentEdit(file, version.get, edits)) + else Nil + } + else Nil + + val (reparse, perspective) = node_perspective(doc_blobs, caret) + if (reparse || pending_edits.nonEmpty || last_perspective != perspective || + workspace_edits.nonEmpty) + { + val prover_edits = node_edits(node_header, pending_edits, perspective) + val edits = (workspace_edits, prover_edits) + Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) + } + else None + } + + + /* publish annotations */ + + def publish(rendering: VSCode_Rendering): + (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = + { + val diagnostics = rendering.diagnostics + val decorations = + if (node_visible) rendering.decorations + else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) } + + val changed_diagnostics = + if (diagnostics == published_diagnostics) None else Some(diagnostics) + val changed_decorations = + if (decorations == published_decorations) None + else if (published_decorations.isEmpty) Some(decorations) + else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) + + (changed_diagnostics, changed_decorations, + copy(published_diagnostics = diagnostics, published_decorations = decorations)) + } + + + /* prover session */ + + def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] + + def is_stable: Boolean = pending_edits.isEmpty + def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) + + def rendering(snapshot: Document.Snapshot): VSCode_Rendering = + new VSCode_Rendering(snapshot, model) + def rendering(): VSCode_Rendering = rendering(snapshot()) + + + /* syntax */ + + def syntax(): Outer_Syntax = + if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty +} diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Nov 28 20:14:46 2020 +0100 @@ -20,14 +20,14 @@ /* decorations */ private def color_decorations(prefix: String, types: Set[Rendering.Color.Value], - colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] = + colors: List[Text.Info[Rendering.Color.Value]]): List[VSCode_Model.Decoration] = { val color_ranges = (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) } types.toList.map(c => - Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) + VSCode_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) } private val background_colors = @@ -42,8 +42,8 @@ private val message_severity = Map( - Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning, - Markup.ERROR -> Protocol.DiagnosticSeverity.Error) + Markup.LEGACY -> LSP.DiagnosticSeverity.Warning, + Markup.ERROR -> LSP.DiagnosticSeverity.Error) /* markup elements */ @@ -65,18 +65,18 @@ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION) } -class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model) +class VSCode_Rendering(snapshot: Document.Snapshot, _model: VSCode_Model) extends Rendering(snapshot, _model.resources.options, _model.session) { rendering => - def model: Document_Model = _model + def model: VSCode_Model = _model def resources: VSCode_Resources = model.resources /* bibtex */ - def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = + def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] = Bibtex.entries_iterator(resources.get_models) def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] = @@ -85,7 +85,7 @@ /* completion */ - def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] = + def completion(caret_pos: Line.Position, caret: Text.Offset): List[LSP.CompletionItem] = { val doc = model.content.doc val line = caret_pos.line @@ -119,7 +119,7 @@ case None => Nil case Some(result) => result.items.map(item => - Protocol.CompletionItem( + LSP.CompletionItem( label = item.replacement, detail = Some(item.description.mkString(" ")), range = Some(doc.range(item.range)))) @@ -146,7 +146,7 @@ case _ => None }).filterNot(info => info.info.is_empty) - def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] = + def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = { (for { Text.Info(text_range, res) <- results.iterator @@ -155,7 +155,7 @@ } yield { val message = resources.output_pretty_message(body) val severity = VSCode_Rendering.message_severity.get(name) - Protocol.Diagnostic(range, message, severity = severity) + LSP.Diagnostic(range, message, severity = severity) }).toList } @@ -212,8 +212,8 @@ /* decorations */ - def decorations: List[Document_Model.Decoration] = // list of canonical length and order - Par_List.map((f: () => List[Document_Model.Decoration]) => f(), + def decorations: List[VSCode_Model.Decoration] = // list of canonical length and order + Par_List.map((f: () => List[VSCode_Model.Decoration]) => f(), List( () => VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors, @@ -232,16 +232,16 @@ dotted(model.content.text_range)))).flatten ::: List(VSCode_Spell_Checker.decoration(rendering)) - def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = + def decoration_output(decoration: VSCode_Model.Decoration): LSP.Decoration = { val content = for (Text.Info(text_range, msgs) <- decoration.content) yield { val range = model.content.doc.range(text_range) - Protocol.DecorationOpts(range, - msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg)))) + LSP.DecorationOpts(range, + msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg)))) } - Protocol.Decoration(decoration.typ, content) + LSP.Decoration(decoration.typ, content) } diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Nov 28 20:14:46 2020 +0100 @@ -19,13 +19,13 @@ /* internal state */ sealed case class State( - models: Map[JFile, Document_Model] = Map.empty, + models: Map[JFile, VSCode_Model] = Map.empty, caret: Option[(JFile, Line.Position)] = None, overlays: Document.Overlays = Document.Overlays.empty, pending_input: Set[JFile] = Set.empty, pending_output: Set[JFile] = Set.empty) { - def update_models(changed: Traversable[(JFile, Document_Model)]): State = + def update_models(changed: Traversable[(JFile, VSCode_Model)]): State = copy( models = models ++ changed, pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, @@ -63,7 +63,7 @@ /* caret */ - sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset) + sealed case class Caret(file: JFile, model: VSCode_Model, offset: Text.Offset) { def node_name: Document.Node.Name = model.node_name } @@ -114,9 +114,9 @@ else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path))) } - def get_models: Map[JFile, Document_Model] = state.value.models - def get_model(file: JFile): Option[Document_Model] = get_models.get(file) - def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) + def get_models: Map[JFile, VSCode_Model] = state.value.models + def get_model(file: JFile): Option[VSCode_Model] = get_models.get(file) + def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name)) /* file content */ @@ -156,7 +156,7 @@ def change_model( session: Session, - editor: Server.Editor, + editor: Language_Server.Editor, file: JFile, version: Long, text: String, @@ -164,7 +164,7 @@ { state.change(st => { - val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) + val model = st.models.getOrElse(file, VSCode_Model.init(session, editor, node_name(file))) val model1 = (model.change_text(text, range) getOrElse model).set_version(version).external(false) st.update_models(Some(file -> model1)) @@ -208,7 +208,7 @@ def resolve_dependencies( session: Session, - editor: Server.Editor, + editor: Language_Server.Editor, file_watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => @@ -252,7 +252,7 @@ text <- { file_watcher.register_parent(file); read_file_content(node_name) } } yield { - val model = Document_Model.init(session, editor, node_name) + val model = VSCode_Model.init(session, editor, node_name) val model1 = (model.change_text(text) getOrElse model).external(true) (file, model1) }).toList @@ -280,7 +280,7 @@ } yield (edits, (file, model1))).toList for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty } - channel.write(Protocol.WorkspaceEdit(workspace_edits)) + channel.write(LSP.WorkspaceEdit(workspace_edits)) session.update(st.document_blobs, changed_models.flatMap(res => res._1._2)) @@ -318,7 +318,7 @@ } yield { for (diags <- changed_diags) - channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags))) + channel.write(LSP.PublishDiagnostics(file, rendering.diagnostics_output(diags))) if (pide_extensions) { for (decos <- changed_decos; deco <- decos) channel.write(rendering.decoration_output(deco).json(file)) diff -r 042180540068 -r 4519eeefe3b5 src/Tools/VSCode/src/vscode_spell_checker.scala --- a/src/Tools/VSCode/src/vscode_spell_checker.scala Sat Nov 28 17:38:03 2020 +0100 +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala Sat Nov 28 20:14:46 2020 +0100 @@ -12,7 +12,7 @@ object VSCode_Spell_Checker { - def decoration(rendering: VSCode_Rendering): Document_Model.Decoration = + def decoration(rendering: VSCode_Rendering): VSCode_Model.Decoration = { val model = rendering.model val ranges = @@ -22,13 +22,13 @@ text <- model.get_text(spell.range).iterator info <- spell_checker.marked_words(spell.range.start, text).iterator } yield info.range).toList - Document_Model.Decoration.ranges("spell_checker", ranges) + VSCode_Model.Decoration.ranges("spell_checker", ranges) } def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] = rendering.resources.spell_checker.get.flatMap(_.completion(rendering, caret)) - def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] = + def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[LSP.CompletionItem] = { val result = for { @@ -40,8 +40,8 @@ result match { case Some((spell_checker, word)) => - def item(command: Protocol.Command): Protocol.CompletionItem = - Protocol.CompletionItem( + def item(command: LSP.Command): LSP.CompletionItem = + LSP.CompletionItem( label = command.title, text = Some(""), range = Some(rendering.model.content.doc.range(Text.Range(caret))), @@ -50,18 +50,18 @@ val update_items = if (spell_checker.check(word)) List( - item(Protocol.Exclude_Word.command), - item(Protocol.Exclude_Word_Permanently.command)) + item(LSP.Exclude_Word.command), + item(LSP.Exclude_Word_Permanently.command)) else List( - item(Protocol.Include_Word.command), - item(Protocol.Include_Word_Permanently.command)) + item(LSP.Include_Word.command), + item(LSP.Include_Word_Permanently.command)) val reset_items = spell_checker.reset_enabled() match { case 0 => Nil case n => - val command = Protocol.Reset_Words.command + val command = LSP.Reset_Words.command List(item(command).copy(label = command.title + " (" + n + ")")) }