--- 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,
--- 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
--- 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
{
--- 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
-}
--- 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())
--- /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)
+ }
+}
--- /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))
+ }
+ }
+}
--- 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
--- 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))
- }
- }
-}
--- 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)
- }
-}
--- 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 */
--- /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
+}
--- 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)
}
--- 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))
--- 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 + ")"))
}