diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,188 +1,188 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Author: Lars Hupel Isabelle system tools: external executables or internal Scala functions. */ package isabelle import java.net.URLClassLoader import scala.reflect.runtime.universe import scala.tools.reflect.{ToolBox,ToolBoxError} object Isabelle_Tool { /* Scala source tools */ abstract class Body extends Function[List[String], Unit] private def compile(path: Path): Body = { def err(msg: String): Nothing = cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) val source = File.read(path) val class_loader = new URLClassLoader(Array(), getClass.getClassLoader) val tool_box = universe.runtimeMirror(class_loader).mkToolBox() try { val symbol = tool_box.parse(source) match { case tree: universe.ModuleDef => tool_box.define(tree) case _ => err("Source does not describe a module (Scala object)") } tool_box.compile(universe.Ident(symbol))() match { case body: Body => body case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } catch { case e: ToolBoxError => if (tool_box.frontEnd.hasErrors) { val infos = tool_box.frontEnd.infos.toList val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) err(msgs.mkString("\n")) } else err(e.toString) } } /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, file_name: String): Boolean = { val file = (dir + Path.explode(file_name)).file try { file.isFile && file.canRead && (file_name.endsWith(".scala") || file.canExecute) && !file_name.endsWith("~") && !file_name.endsWith(".orig") } catch { case _: SecurityException => false } } private def list_external(): List[(String, String)] = { val Description = """.*\bDESCRIPTION: *(.*)""".r for { dir <- dirs() if dir.is_dir file_name <- File.read_dir(dir) if is_external(dir, file_name) } yield { val source = File.read(dir + Path.explode(file_name)) val name = Library.perhaps_unsuffix(".scala", file_name) val description = split_lines(source).collectFirst({ case Description(s) => s }) getOrElse "" (name, description) } } private def find_external(name: String): Option[List[String] => Unit] = dirs().collectFirst({ case dir if is_external(dir, name + ".scala") => compile(dir + Path.explode(name + ".scala")) case dir if is_external(dir, name) => (args: List[String]) => { val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) private def list_internal(): List[(String, String)] = for (tool <- internal_tools.toList) yield (tool.name, tool.description) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool { tool.body(args) } }) /* command line entry point */ def main(args: Array[String]) { Command_Line.tool { args.toList match { case Nil | List("-?") => val tool_descriptions = (list_external() ::: list_internal()).sortBy(_._1). map({ case (a, "") => a case (a, b) => a + " - " + b }) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service class Tools extends Isabelle_Scala_Tools( Build.isabelle_tool, Build_Docker.isabelle_tool, Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, ML_Process.isabelle_tool, Mercurial.isabelle_tool, Mkroot.isabelle_tool, Options.isabelle_tool, Phabricator.isabelle_tool1, Phabricator.isabelle_tool2, Phabricator.isabelle_tool3, Phabricator.isabelle_tool4, Presentation.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Sessions.isabelle_tool, Scala_Project.isabelle_tool, Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, 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, Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_E.isabelle_tool, Build_Fonts.isabelle_tool, Build_JDK.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, Build_SPASS.isabelle_tool, Build_SQLite.isabelle_tool, Build_Status.isabelle_tool, Build_VeriT.isabelle_tool, Build_Zipperposition.isabelle_tool, Check_Sources.isabelle_tool, Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,320 +1,320 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( src/HOL/SPARK/Tools/spark.scala src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala src/Pure/Admin/build_cygwin.scala src/Pure/Admin/build_doc.scala src/Pure/Admin/build_e.scala src/Pure/Admin/build_fonts.scala src/Pure/Admin/build_history.scala src/Pure/Admin/build_jdk.scala src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala src/Pure/Admin/build_spass.scala src/Pure/Admin/build_sqlite.scala src/Pure/Admin/build_status.scala src/Pure/Admin/build_verit.scala src/Pure/Admin/build_zipperposition.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala src/Pure/Concurrent/mailbox.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/synchronized.scala src/Pure/GUI/color_value.scala src/Pure/GUI/gui.scala src/Pure/GUI/gui_thread.scala src/Pure/GUI/popup.scala src/Pure/GUI/wrap_panel.scala src/Pure/General/antiquote.scala src/Pure/General/bytes.scala src/Pure/General/cache.scala src/Pure/General/codepoint.scala src/Pure/General/comment.scala src/Pure/General/completion.scala src/Pure/General/csv.scala src/Pure/General/date.scala src/Pure/General/exn.scala src/Pure/General/file.scala src/Pure/General/file_watcher.scala src/Pure/General/graph.scala src/Pure/General/graph_display.scala src/Pure/General/graphics_file.scala src/Pure/General/http.scala src/Pure/General/json.scala src/Pure/General/linear_set.scala src/Pure/General/logger.scala src/Pure/General/long_name.scala src/Pure/General/mailman.scala src/Pure/General/mercurial.scala src/Pure/General/multi_map.scala src/Pure/General/output.scala src/Pure/General/path.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/General/properties.scala src/Pure/General/rdf.scala src/Pure/General/scan.scala src/Pure/General/sha1.scala src/Pure/General/sql.scala src/Pure/General/ssh.scala src/Pure/General/symbol.scala src/Pure/General/time.scala src/Pure/General/timing.scala src/Pure/General/untyped.scala src/Pure/General/url.scala src/Pure/General/utf8.scala src/Pure/General/uuid.scala src/Pure/General/value.scala src/Pure/General/word.scala src/Pure/General/xz.scala src/Pure/Isar/document_structure.scala src/Pure/Isar/keyword.scala src/Pure/Isar/line_structure.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.scala src/Pure/Isar/token.scala src/Pure/ML/ml_console.scala src/Pure/ML/ml_lex.scala src/Pure/ML/ml_process.scala src/Pure/ML/ml_statistics.scala src/Pure/ML/ml_syntax.scala src/Pure/PIDE/byte_message.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.scala src/Pure/PIDE/document_status.scala src/Pure/PIDE/editor.scala src/Pure/PIDE/headless.scala src/Pure/PIDE/line.scala src/Pure/PIDE/markup.scala src/Pure/PIDE/markup_tree.scala src/Pure/PIDE/protocol.scala src/Pure/PIDE/protocol_handlers.scala src/Pure/PIDE/protocol_message.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/query_operation.scala src/Pure/PIDE/rendering.scala src/Pure/PIDE/resources.scala src/Pure/PIDE/session.scala src/Pure/PIDE/text.scala src/Pure/PIDE/xml.scala src/Pure/PIDE/yxml.scala src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala src/Pure/System/cygwin.scala src/Pure/System/distribution.scala src/Pure/System/executable.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_platform.scala src/Pure/System/isabelle_process.scala src/Pure/System/isabelle_system.scala src/Pure/System/isabelle_tool.scala src/Pure/System/java_statistics.scala src/Pure/System/linux.scala src/Pure/System/mingw.scala src/Pure/System/numa.scala src/Pure/System/options.scala src/Pure/System/platform.scala src/Pure/System/posix_interrupt.scala src/Pure/System/process_result.scala src/Pure/System/progress.scala src/Pure/System/scala.scala src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala src/Pure/Thy/html.scala src/Pure/Thy/latex.scala src/Pure/Thy/presentation.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_element.scala src/Pure/Thy/thy_header.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/build_docker.scala src/Pure/Tools/build_job.scala src/Pure/Tools/check_keywords.scala src/Pure/Tools/debugger.scala src/Pure/Tools/doc.scala src/Pure/Tools/dump.scala src/Pure/Tools/fontforge.scala src/Pure/Tools/main.scala src/Pure/Tools/mkroot.scala src/Pure/Tools/phabricator.scala src/Pure/Tools/print_operation.scala src/Pure/Tools/profiling_report.scala src/Pure/Tools/scala_project.scala src/Pure/Tools/server.scala src/Pure/Tools/server_commands.scala src/Pure/Tools/simplifier_trace.scala src/Pure/Tools/spell_checker.scala src/Pure/Tools/task_statistics.scala src/Pure/Tools/update.scala src/Pure/Tools/update_cartouches.scala src/Pure/Tools/update_comments.scala src/Pure/Tools/update_header.scala src/Pure/Tools/update_then.scala src/Pure/Tools/update_theorems.scala src/Pure/library.scala src/Pure/pure_thy.scala src/Pure/term.scala src/Pure/term_xml.scala src/Pure/thm_name.scala src/Tools/Graphview/graph_file.scala src/Tools/Graphview/graph_panel.scala src/Tools/Graphview/graphview.scala src/Tools/Graphview/layout.scala src/Tools/Graphview/main_panel.scala src/Tools/Graphview/metrics.scala src/Tools/Graphview/model.scala src/Tools/Graphview/mutator.scala src/Tools/Graphview/mutator_dialog.scala src/Tools/Graphview/mutator_event.scala src/Tools/Graphview/popups.scala src/Tools/Graphview/shapes.scala 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 ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## target TARGET_DIR="lib/classes" TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" function target_shasum() { shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null } function target_clean() { rm -rf "$TARGET_DIR" } [ -n "$FRESH" ] && target_clean ## build target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ "$?" -ne 0 ]; then echo "### Building Isabelle/Scala ..." target_clean BUILD_DIR="$TARGET_DIR/build" mkdir -p "$BUILD_DIR" ( export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ -d "$BUILD_DIR" "${SOURCES[@]}" ) || fail "Failed to compile sources" CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ -C "$BUILD_DIR" META-INF \ -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" rm -rf "$BUILD_DIR" target_shasum > "$TARGET_SHASUM" fi diff --git a/src/Tools/VSCode/src/channel.scala b/src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala +++ b/src/Tools/VSCode/src/channel.scala @@ -1,108 +1,108 @@ /* Title: Tools/VSCode/src/channel.scala Author: Makarius Channel with JSON RPC protocol. */ package isabelle.vscode import isabelle._ import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile} import scala.collection.mutable class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false) { /* read message */ private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r private def read_line(): String = Byte_Message.read_line(in) match { case Some(bytes) => bytes.text case None => "" } private def read_header(): List[String] = { val header = new mutable.ListBuffer[String] var line = "" while ({ line = read_line(); line != "" }) header += line header.toList } private def read_content(n: Int): String = { val bytes = Bytes.read_stream(in, limit = n) if (bytes.length == n) bytes.text else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)") } def read(): Option[JSON.T] = { read_header() match { case Nil => None case Content_Length(s) :: _ => s match { 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) } case header => error(cat_lines("Malformed header:" :: header)) } } /* write message */ def write(json: JSON.T) { val msg = JSON.Format(json) val content = UTF8.bytes(msg) 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) out.flush } } /* 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 { def apply(msg: => String) { log_error_message(msg) } } /* progress */ def progress(verbose: Boolean = false): Progress = new Progress { override def echo(msg: String): Unit = log_writeln(msg) override def echo_warning(msg: String): Unit = log_warning(msg) override def echo_error_message(msg: String): Unit = log_error_message(msg) override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) } } diff --git a/src/Tools/VSCode/src/dynamic_output.scala b/src/Tools/VSCode/src/dynamic_output.scala --- a/src/Tools/VSCode/src/dynamic_output.scala +++ b/src/Tools/VSCode/src/dynamic_output.scala @@ -1,80 +1,80 @@ /* Title: Tools/VSCode/src/dynamic_output.scala Author: Makarius Dynamic output, depending on caret focus: messages, state etc. */ package isabelle.vscode import isabelle._ object Dynamic_Output { sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil) { def handle_update( resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State = { val st1 = resources.get_caret() match { case None => copy(output = Nil) case Some(caret) => val snapshot = caret.model.snapshot() if (do_update && !snapshot.is_outdated) { snapshot.current_command(caret.node_name, caret.offset) match { case None => copy(output = Nil) case Some(command) => copy(output = if (restriction.isEmpty || restriction.get.contains(command)) Rendering.output_messages(snapshot.command_results(command)) else output) } } 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()) private def handle_update(restriction: Option[Set[Command]]) { state.change(_.handle_update(server.resources, server.channel, restriction)) } /* main */ private val main = Session.Consumer[Any](getClass.getName) { case changed: Session.Commands_Changed => handle_update(if (changed.assignment) None else Some(changed.commands)) case Session.Caret_Focus => handle_update(None) } def init() { server.session.commands_changed += main server.session.caret_focus += main handle_update(None) } def exit() { server.session.commands_changed -= main server.session.caret_focus -= main } } diff --git a/src/Tools/VSCode/src/server.scala b/src/Tools/VSCode/src/language_server.scala rename from src/Tools/VSCode/src/server.scala rename to src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/server.scala +++ b/src/Tools/VSCode/src/language_server.scala @@ -1,560 +1,559 @@ -/* Title: Tools/VSCode/src/server.scala +/* 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 Server +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 Server(channel, options, session_name = logic, session_dirs = dirs, + 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 Server( +class Language_Server( val channel: Channel, options: Options, - session_name: String = Server.default_logic, + 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[Protocol.TextDocumentChange]) + private def change_document(file: JFile, version: Long, changes: List[LSP.TextDocumentChange]) { - val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] - @tailrec def norm(chs: List[Protocol.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: Protocol.Id) + def init(id: LSP.Id) { def reply_ok(msg: String) { - channel.write(Protocol.Initialize.reply(id, "")) + channel.write(LSP.Initialize.reply(id, "")) channel.writeln(msg) } def reply_error(msg: String) { - channel.write(Protocol.Initialize.reply(id, msg)) + 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: Protocol.Id) + def shutdown(id: LSP.Id) { - def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) + 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: Protocol.Id, node_pos: Line.Node_Position) + 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(Protocol.Completion.reply(id, result)) + 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: Protocol.Id, node_pos: Line.Node_Position) + 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 => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) + val contents = info.info.map(t => LSP.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } - channel.write(Protocol.Hover.reply(id, result)) + channel.write(LSP.Hover.reply(id, result)) } /* goto definition */ - def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) + 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(Protocol.GotoDefinition.reply(id, result)) + channel.write(LSP.GotoDefinition.reply(id, result)) } /* document highlights */ - def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) + 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 => Protocol.DocumentHighlight.text(model.content.doc.range(r))) + .map(r => LSP.DocumentHighlight.text(model.content.doc.range(r))) }) getOrElse Nil - channel.write(Protocol.DocumentHighlights.reply(id, result)) + 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 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))) + 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 Protocol.DidChangeTextDocument(file, version, changes) => + case LSP.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") + 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 Server.Editor + 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(Protocol.Caret_Update(node_pos, focus)) } + def follow(unit: Unit) { channel.write(LSP.Caret_Update(node_pos, focus)) } }) } /* dispatcher thread */ override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) } } diff --git a/src/Tools/VSCode/src/protocol.scala b/src/Tools/VSCode/src/lsp.scala rename from src/Tools/VSCode/src/protocol.scala rename to src/Tools/VSCode/src/lsp.scala --- a/src/Tools/VSCode/src/protocol.scala +++ b/src/Tools/VSCode/src/lsp.scala @@ -1,626 +1,626 @@ -/* Title: Tools/VSCode/src/protocol.scala +/* 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 Protocol +object LSP { /* abstract message */ object Message { val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0") def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean) { val header = json match { case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id") case _ => JSON.Object.empty } if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json)) else logger(prefix + " " + JSON.Format(header)) } } /* notification */ object Notification { def apply(method: String, params: JSON.T): JSON.T = Message.empty + ("method" -> method) + ("params" -> params) def unapply(json: JSON.T): Option[(String, Option[JSON.T])] = for { method <- JSON.string(json, "method") params = JSON.value(json, "params") } yield (method, params) } class Notification0(name: String) { def unapply(json: JSON.T): Option[Unit] = json match { case Notification(method, _) if method == name => Some(()) case _ => None } } /* request message */ object Id { def empty: Id = Id("") } sealed case class Id(id: Any) { require( id.isInstanceOf[Int] || id.isInstanceOf[Long] || id.isInstanceOf[Double] || id.isInstanceOf[String]) override def toString: String = id.toString } object RequestMessage { def apply(id: Id, method: String, params: JSON.T): JSON.T = Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params) def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] = for { id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id") method <- JSON.string(json, "method") params = JSON.value(json, "params") } yield (Id(id), method, params) } class Request0(name: String) { def unapply(json: JSON.T): Option[Id] = json match { case RequestMessage(id, method, _) if method == name => Some(id) case _ => None } } class RequestTextDocumentPosition(name: String) { def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] = json match { case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name => Some((id, node_pos)) case _ => None } } /* response message */ object ResponseMessage { def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T = Message.empty + ("id" -> id.id) ++ JSON.optional("result" -> result) ++ JSON.optional("error" -> error.map(_.json)) def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T = if (error == "") apply(id, result = result) else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error))) def is_empty(json: JSON.T): Boolean = JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined } sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) { def json: JSON.T = JSON.Object("code" -> code, "message" -> message) ++ JSON.optional("data" -> data) } object ErrorCodes { val ParseError = -32700 val InvalidRequest = -32600 val MethodNotFound = -32601 val InvalidParams = -32602 val InternalError = -32603 val serverErrorStart = -32099 val serverErrorEnd = -32000 } /* init and exit */ object Initialize extends Request0("initialize") { def reply(id: Id, error: String): JSON.T = ResponseMessage.strict( id, Some(JSON.Object("capabilities" -> ServerCapabilities.json)), error) } object ServerCapabilities { val json: JSON.T = JSON.Object( "textDocumentSync" -> 2, "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil), "hoverProvider" -> true, "definitionProvider" -> true, "documentHighlightProvider" -> true) } object Initialized extends Notification0("initialized") object Shutdown extends Request0("shutdown") { def reply(id: Id, error: String): JSON.T = ResponseMessage.strict(id, Some("OK"), error) } object Exit extends Notification0("exit") /* document positions */ object Position { def apply(pos: Line.Position): JSON.T = JSON.Object("line" -> pos.line, "character" -> pos.column) def unapply(json: JSON.T): Option[Line.Position] = for { line <- JSON.int(json, "line") column <- JSON.int(json, "character") } yield Line.Position(line, column) } object Range { def compact(range: Line.Range): List[Int] = List(range.start.line, range.start.column, range.stop.line, range.stop.column) def apply(range: Line.Range): JSON.T = JSON.Object("start" -> Position(range.start), "end" -> Position(range.stop)) def unapply(json: JSON.T): Option[Line.Range] = (JSON.value(json, "start"), JSON.value(json, "end")) match { case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop)) case _ => None } } object Location { def apply(loc: Line.Node_Range): JSON.T = JSON.Object("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range)) def unapply(json: JSON.T): Option[Line.Node_Range] = for { uri <- JSON.string(json, "uri") range_json <- JSON.value(json, "range") range <- Range.unapply(range_json) } yield Line.Node_Range(Url.absolute_file_name(uri), range) } object TextDocumentPosition { def unapply(json: JSON.T): Option[Line.Node_Position] = for { doc <- JSON.value(json, "textDocument") uri <- JSON.string(doc, "uri") pos_json <- JSON.value(json, "position") pos <- Position.unapply(pos_json) } yield Line.Node_Position(Url.absolute_file_name(uri), pos) } /* marked strings */ sealed case class MarkedString(text: String, language: String = "plaintext") { def json: JSON.T = JSON.Object("language" -> language, "value" -> text) } object MarkedStrings { def json(msgs: List[MarkedString]): Option[JSON.T] = msgs match { case Nil => None case List(msg) => Some(msg.json) case _ => Some(msgs.map(_.json)) } } /* diagnostic messages */ object MessageType { val Error = 1 val Warning = 2 val Info = 3 val Log = 4 } object DisplayMessage { def apply(message_type: Int, message: String, show: Boolean = true): JSON.T = Notification(if (show) "window/showMessage" else "window/logMessage", JSON.Object("type" -> message_type, "message" -> message)) } /* commands */ sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) { def json: JSON.T = JSON.Object("title" -> title, "command" -> command, "arguments" -> arguments) } /* document edits */ object DidOpenTextDocument { def unapply(json: JSON.T): Option[(JFile, String, Long, String)] = json match { case Notification("textDocument/didOpen", Some(params)) => for { doc <- JSON.value(params, "textDocument") uri <- JSON.string(doc, "uri") lang <- JSON.string(doc, "languageId") version <- JSON.long(doc, "version") text <- JSON.string(doc, "text") } yield (Url.absolute_file(uri), lang, version, text) case _ => None } } sealed case class TextDocumentChange(range: Option[Line.Range], text: String) object DidChangeTextDocument { def unapply_change(json: JSON.T): Option[TextDocumentChange] = for { text <- JSON.string(json, "text") } yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text) def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] = json match { case Notification("textDocument/didChange", Some(params)) => for { doc <- JSON.value(params, "textDocument") uri <- JSON.string(doc, "uri") version <- JSON.long(doc, "version") changes <- JSON.list(params, "contentChanges", unapply_change _) } yield (Url.absolute_file(uri), version, changes) case _ => None } } class TextDocumentNotification(name: String) { def unapply(json: JSON.T): Option[JFile] = json match { case Notification(method, Some(params)) if method == name => for { doc <- JSON.value(params, "textDocument") uri <- JSON.string(doc, "uri") } yield Url.absolute_file(uri) case _ => None } } object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose") object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") /* workspace edits */ sealed case class TextEdit(range: Line.Range, new_text: String) { def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text) } sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) { def json: JSON.T = JSON.Object( "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version), "edits" -> edits.map(_.json)) } object WorkspaceEdit { def apply(edits: List[TextDocumentEdit]): JSON.T = RequestMessage(Id.empty, "workspace/applyEdit", JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json)))) } /* completion */ sealed case class CompletionItem( label: String, kind: Option[Int] = None, detail: Option[String] = None, documentation: Option[String] = None, text: Option[String] = None, range: Option[Line.Range] = None, command: Option[Command] = None) { def json: JSON.T = JSON.Object("label" -> label) ++ JSON.optional("kind" -> kind) ++ JSON.optional("detail" -> detail) ++ JSON.optional("documentation" -> documentation) ++ JSON.optional("insertText" -> text) ++ JSON.optional("range" -> range.map(Range(_))) ++ JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++ JSON.optional("command" -> command.map(_.json)) } object Completion extends RequestTextDocumentPosition("textDocument/completion") { def reply(id: Id, result: List[CompletionItem]): JSON.T = ResponseMessage(id, Some(result.map(_.json))) } /* spell checker */ object Include_Word extends Notification0("PIDE/include_word") { val command = Command("Include word", "isabelle.include-word") } object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") { val command = Command("Include word permanently", "isabelle.include-word-permanently") } object Exclude_Word extends Notification0("PIDE/exclude_word") { val command = Command("Exclude word", "isabelle.exclude-word") } object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") { val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently") } object Reset_Words extends Notification0("PIDE/reset_words") { val command = Command("Reset non-permanent words", "isabelle.reset-words") } /* hover request */ object Hover extends RequestTextDocumentPosition("textDocument/hover") { def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T = { val res = result match { case Some((range, contents)) => JSON.Object( "contents" -> MarkedStrings.json(contents).getOrElse(Nil), "range" -> Range(range)) case None => JSON.Object("contents" -> Nil) } ResponseMessage(id, Some(res)) } } /* goto definition request */ object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") { def reply(id: Id, result: List[Line.Node_Range]): JSON.T = ResponseMessage(id, Some(result.map(Location.apply(_)))) } /* document highlights request */ object DocumentHighlight { def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1)) def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2)) def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3)) } sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) { def json: JSON.T = kind match { case None => JSON.Object("range" -> Range(range)) case Some(k) => JSON.Object("range" -> Range(range), "kind" -> k) } } object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") { def reply(id: Id, result: List[DocumentHighlight]): JSON.T = ResponseMessage(id, Some(result.map(_.json))) } /* diagnostics */ sealed case class Diagnostic(range: Line.Range, message: String, severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None) { def json: JSON.T = Message.empty + ("range" -> Range(range)) + ("message" -> message) ++ JSON.optional("severity" -> severity) ++ JSON.optional("code" -> code) ++ JSON.optional("source" -> source) } object DiagnosticSeverity { val Error = 1 val Warning = 2 val Information = 3 val Hint = 4 } object PublishDiagnostics { def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T = Notification("textDocument/publishDiagnostics", JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json))) } /* decorations */ sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString]) { def json: JSON.T = JSON.Object("range" -> Range.compact(range)) ++ JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) } sealed case class Decoration(typ: String, content: List[DecorationOpts]) { def json(file: JFile): JSON.T = Notification("PIDE/decoration", JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) } /* caret update: bidirectional */ object Caret_Update { def apply(node_pos: Line.Node_Position, focus: Boolean): JSON.T = Notification("PIDE/caret_update", JSON.Object( "uri" -> Url.print_file_name(node_pos.name), "line" -> node_pos.pos.line, "character" -> node_pos.pos.column, "focus" -> focus)) def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] = json match { case Notification("PIDE/caret_update", Some(params)) => val caret = for { uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri) pos <- Position.unapply(params) } yield (Url.absolute_file(uri), pos) Some(caret) case _ => None } } /* dynamic output */ object Dynamic_Output { def apply(content: String): JSON.T = Notification("PIDE/dynamic_output", JSON.Object("content" -> content)) } /* state output */ object State_Output { def apply(id: Counter.ID, content: String): JSON.T = Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content)) } class State_Id_Notification(name: String) { def unapply(json: JSON.T): Option[Counter.ID] = json match { case Notification(method, Some(params)) if method == name => JSON.long(params, "id") case _ => None } } object State_Init extends Notification0("PIDE/state_init") object State_Exit extends State_Id_Notification("PIDE/state_exit") object State_Locate extends State_Id_Notification("PIDE/state_locate") object State_Update extends State_Id_Notification("PIDE/state_update") object State_Auto_Update { def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] = json match { case Notification("PIDE/state_auto_update", Some(params)) => for { id <- JSON.long(params, "id") enabled <- JSON.bool(params, "enabled") } yield (id, enabled) case _ => None } } /* preview */ object Preview_Request { def unapply(json: JSON.T): Option[(JFile, Int)] = json match { case Notification("PIDE/preview_request", Some(params)) => for { uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri) column <- JSON.int(params, "column") } yield (Url.absolute_file(uri), column) case _ => None } } object Preview_Response { def apply(file: JFile, column: Int, label: String, content: String): JSON.T = Notification("PIDE/preview_response", JSON.Object( "uri" -> Url.print_file(file), "column" -> column, "label" -> label, "content" -> content)) } /* Isabelle symbols */ object Symbols_Request extends Notification0("PIDE/symbols_request") object Symbols { def apply(): JSON.T = { val entries = for ((sym, code) <- Symbol.codes) yield JSON.Object("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code) Notification("PIDE/symbols", JSON.Object("entries" -> entries)) } } } diff --git a/src/Tools/VSCode/src/preview_panel.scala b/src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala +++ b/src/Tools/VSCode/src/preview_panel.scala @@ -1,44 +1,43 @@ /* Title: Tools/VSCode/src/preview_panel.scala Author: Makarius HTML document preview. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} class Preview_Panel(resources: VSCode_Resources) { private val pending = Synchronized(Map.empty[JFile, Int]) def request(file: JFile, column: Int): Unit = pending.change(map => map + (file -> column)) def flush(channel: Channel): Boolean = { pending.change_result(map => { val map1 = (map /: map.iterator)({ case (m, (file, column)) => resources.get_model(file) match { case Some(model) => val snapshot = model.snapshot() 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 } }) (map1.nonEmpty, map1) }) } } diff --git a/src/Tools/VSCode/src/state_panel.scala b/src/Tools/VSCode/src/state_panel.scala --- a/src/Tools/VSCode/src/state_panel.scala +++ b/src/Tools/VSCode/src/state_panel.scala @@ -1,173 +1,173 @@ /* Title: Tools/VSCode/src/state_panel.scala Author: Makarius Show proof state. */ package isabelle.vscode import isabelle._ object State_Panel { 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)) instance.init() } def exit(id: Counter.ID) { instances.change(map => map.get(id) match { case None => map case Some(instance) => instance.exit(); map - id }) } def locate(id: Counter.ID): Unit = instances.value.get(id).foreach(state => state.server.editor.send_dispatcher(state.locate())) def update(id: Counter.ID): Unit = instances.value.get(id).foreach(state => state.server.editor.send_dispatcher(state.update())) def auto_update(id: Counter.ID, enabled: Boolean): Unit = instances.value.get(id).foreach(state => state.server.editor.send_dispatcher(state.auto_update(Some(enabled)))) } -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 */ private val output_active = Synchronized(true) private val print_state = new Query_Operation(server.editor, (), "print_state", _ => (), (snapshot, results, body) => if (output_active.value) { val text = server.resources.output_pretty_message(Pretty.separate(body)) val content = HTML.output_document( List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css), HTML.script(controls_script)), List(controls, HTML.source(text)), css = "", structural = true) output(content) }) def locate() { print_state.locate_query() } def update() { server.editor.current_node_snapshot(()) match { case Some(snapshot) => (server.editor.current_command((), snapshot), print_state.get_location) match { case (Some(command1), Some(command2)) if command1.id == command2.id => case _ => print_state.apply_query(Nil) } case None => } } /* auto update */ private val auto_update_enabled = Synchronized(true) def auto_update(set: Option[Boolean] = None) { val enabled = auto_update_enabled.guarded_access(a => set match { case None => Some((a, a)) case Some(b) => Some((b, b)) }) if (enabled) update() } /* controls */ private def controls_script = """ const vscode = acquireVsCodeApi(); function invoke_auto_update(enabled) { vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) } function invoke_update() { vscode.postMessage({'command': 'update'}) } function invoke_locate() { vscode.postMessage({'command': 'locate'}) } """ private def auto_update_button: XML.Elem = HTML.GUI.checkbox(HTML.text("Auto update"), name = "auto_update", tooltip = "Indicate automatic update following cursor movement", selected = auto_update_enabled.value, script = "invoke_auto_update(this.checked)") private def update_button: XML.Elem = HTML.GUI.button(List(HTML.bold(HTML.text("Update"))), name = "update", tooltip = "Update display according to the command at cursor position", script = "invoke_update()") private def locate_button: XML.Elem = HTML.GUI.button(HTML.text("Locate"), name = "locate", tooltip = "Locate printed command within source text", script = "invoke_locate()") private def controls: XML.Elem = HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button)) /* main */ private val main = Session.Consumer[Any](getClass.getName) { case changed: Session.Commands_Changed => if (changed.assignment) auto_update() case Session.Caret_Focus => auto_update() } def init() { server.session.commands_changed += main server.session.caret_focus += main server.editor.send_wait_dispatcher { print_state.activate() } server.editor.send_dispatcher { auto_update() } } def exit() { output_active.change(_ => false) server.session.commands_changed -= main server.session.caret_focus -= main server.editor.send_wait_dispatcher { print_state.deactivate() } } } diff --git a/src/Tools/VSCode/src/document_model.scala b/src/Tools/VSCode/src/vscode_model.scala rename from src/Tools/VSCode/src/document_model.scala rename to src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/document_model.scala +++ b/src/Tools/VSCode/src/vscode_model.scala @@ -1,245 +1,248 @@ -/* Title: Tools/VSCode/src/document_model.scala +/* Title: Tools/VSCode/src/vscode_model.scala Author: Makarius -Document model for line-oriented text. +VSCode document model for line-oriented text. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} -object Document_Model +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[Protocol.TextEdit] = + 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)) - Protocol.TextEdit(range, text1) + LSP.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, + 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 Document_Model( +sealed case class VSCode_Model( session: Session, - editor: Server.Editor, + editor: Language_Server.Editor, node_name: Document.Node.Name, - content: Document_Model.Content, + 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[Document_Model.Decoration] = Nil) extends Document.Model + 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): Document_Model = copy(version = Some(new_version)) + def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version)) /* external file */ - def external(b: Boolean): Document_Model = copy(external_file = b) + 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[Document_Model] = + 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 = Document_Model.Content(Line.Document(insert)) + 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 = Document_Model.Content(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[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] = + : 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(Protocol.TextDocumentEdit(file, version.get, edits)) + 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[Document_Model.Decoration]], Document_Model) = + (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 Document_Model.Decoration.empty(deco.typ) } + else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) } val changed_diagnostics = if (diagnostics == published_diagnostics) None else Some(diagnostics) val changed_decorations = if (decorations == published_decorations) None else if (published_decorations.isEmpty) Some(decorations) else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) (changed_diagnostics, changed_decorations, copy(published_diagnostics = diagnostics, published_decorations = decorations)) } /* prover session */ def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) def rendering(snapshot: Document.Snapshot): VSCode_Rendering = new VSCode_Rendering(snapshot, model) def rendering(): VSCode_Rendering = rendering(snapshot()) /* syntax */ def syntax(): Outer_Syntax = if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty } diff --git a/src/Tools/VSCode/src/vscode_rendering.scala b/src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala +++ b/src/Tools/VSCode/src/vscode_rendering.scala @@ -1,330 +1,330 @@ /* Title: Tools/VSCode/src/vscode_rendering.scala Author: Makarius Isabelle/VSCode-specific implementation of quasi-abstract rendering and markup interpretation. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} import scala.annotation.tailrec object VSCode_Rendering { /* 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 = Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result - Rendering.Color.entity private val dotted_colors = Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) /* diagnostic messages */ 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 */ private val diagnostics_elements = Markup.Elements(Markup.LEGACY, Markup.ERROR) private val background_elements = Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements private val dotted_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) val tooltip_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++ Rendering.tooltip_elements private val hyperlink_elements = 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] = Bibtex.completion(history, rendering, caret, resources.get_models) /* 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 doc.offset(Line.Position(line)) match { case None => Nil case Some(line_start) => val history = Completion.History.empty val caret_range = before_caret_range(caret) val syntax = model.syntax() val syntax_completion = syntax.complete(history, unicode = false, explicit = true, line_start, doc.lines(line).text, caret - line_start, language_context(caret_range) getOrElse syntax.language_context) val (no_completion, semantic_completion) = rendering.semantic_completion_result( history, false, syntax_completion.map(_.range), caret_range) if (no_completion) Nil else { val results = Completion.Result.merge(history, semantic_completion, syntax_completion, VSCode_Spell_Checker.completion(rendering, caret), path_completion(caret), bibtex_completion(history, caret)) val items = results match { 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)))) } items ::: VSCode_Spell_Checker.menu_items(rendering, caret) } } } /* diagnostics */ def diagnostics: List[Text.Info[Command.Results]] = snapshot.cumulate[Command.Results]( model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, command_states => { case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body))) if body.nonEmpty => Some(res + (i -> msg)) case (res, Text.Info(_, msg)) => Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _) 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 range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } 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 } /* text color */ def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = { snapshot.select(range, Rendering.text_color_elements, _ => { case Text.Info(_, XML.Elem(Markup(name, props), _)) => if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None else Rendering.text_color.get(name) }) } /* text overview color */ private sealed case class Color_Info( color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int) def text_overview_color: List[Text.Info[Rendering.Color.Value]] = { @tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info]) : List[Text.Info[Rendering.Color.Value]] = { if (lines.nonEmpty) { val end_offset = offset + lines.head.text.length val colors1 = (overview_color(Text.Range(offset, end_offset)), colors) match { case (Some(color), old :: rest) if color == old.color && line == old.end_line => old.copy(end_offset = end_offset, end_line = line + 1) :: rest case (Some(color), _) => Color_Info(color, offset, end_offset, line + 1) :: colors case (None, _) => colors } loop(end_offset + 1, line + 1, lines.tail, colors1) } else { colors.reverse.map(info => Text.Info(Text.Range(info.offset, info.end_offset), info.color)) } } loop(0, 0, model.content.doc.lines, Nil) } /* dotted underline */ def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(VSCode_Rendering.dotted_elements, range) /* 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, background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)), () => VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, foreground(model.content.text_range)), () => VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, text_color(model.content.text_range)), () => VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors, text_overview_color), () => VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, 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) } /* tooltips */ override def timing_threshold: Double = options.real("vscode_timing_threshold") /* hyperlinks */ def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) : Option[Line.Node_Range] = { for { platform_path <- resources.source_file(source_name) file <- (try { Some(File.absolute(new JFile(platform_path))) } catch { case ERROR(_) => None }) } yield { Line.Node_Range(file.getPath, if (range.start > 0) { resources.get_file_content(resources.node_name(file)) match { case Some(text) => val chunk = Symbol.Text_Chunk(text) val doc = Line.Document(text) doc.range(chunk.decode(range)) case _ => Line.Range(Line.Position((line1 - 1) max 0)) } } else Line.Range(Line.Position((line1 - 1) max 0))) } } def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = { if (snapshot.is_outdated) None else for { start <- snapshot.find_command_position(id, range.start) stop <- snapshot.find_command_position(id, range.stop) } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) } def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = pos match { case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) case Position.Item_Id(id, range) => hyperlink_command(id, range) case _ => None } def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = pos match { case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) case _ => None } def hyperlinks(range: Text.Range): List[Line.Node_Range] = { snapshot.cumulate[List[Line.Node_Range]]( range, Nil, VSCode_Rendering.hyperlink_elements, _ => { case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) Some(Line.Node_Range(file) :: links) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => hyperlink_def_position(props).map(_ :: links) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => hyperlink_position(props).map(_ :: links) case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => val iterator = for { Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator() if entry == name } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _)) case _ => None }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } } } diff --git a/src/Tools/VSCode/src/vscode_resources.scala b/src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala +++ b/src/Tools/VSCode/src/vscode_resources.scala @@ -1,373 +1,373 @@ /* Title: Tools/VSCode/src/vscode_resources.scala Author: Makarius Resources for VSCode Language Server: file-system access and global state. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} import scala.util.parsing.input.Reader object VSCode_Resources { /* 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 }, pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) def update_caret(new_caret: Option[(JFile, Line.Position)]): State = if (caret == new_caret) this else copy( caret = new_caret, pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1)) def get_caret(file: JFile): Option[Line.Position] = caret match { case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos) case _ => None } lazy val document_blobs: Document.Blobs = Document.Blobs( (for { (_, model) <- models.iterator blob <- model.get_blob } yield (model.node_name -> blob)).toMap) def change_overlay(insert: Boolean, file: JFile, command: Command, fn: String, args: List[String]): State = copy( overlays = if (insert) overlays.insert(command, fn, args) else overlays.remove(command, fn, args), pending_input = pending_input + file) } /* 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 } } class VSCode_Resources( val options: Options, session_base_info: Sessions.Base_Info, log: Logger = No_Logger) extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log) { resources => private val state = Synchronized(VSCode_Resources.State()) /* options */ def pide_extensions: Boolean = options.bool("vscode_pide_extensions") def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") def tooltip_margin: Int = options.int("vscode_tooltip_margin") def message_margin: Int = options.int("vscode_message_margin") /* document node name */ def node_file(name: Document.Node.Name): JFile = new JFile(name.node) def node_name(file: JFile): Document.Node.Name = find_theory(file) getOrElse { val node = file.getPath val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { val master_dir = file.getParent Document.Node.Name(node, master_dir, theory) } } override def append(dir: String, source_path: Path): String = { val path = source_path.expand if (dir == "" || path.is_absolute) File.platform_path(path) else if (path.is_current) dir else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) dir + JFile.separator + File.platform_path(path) else if (path.is_basic) dir + File.platform_path(path) 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 */ def read_file_content(name: Document.Node.Name): Option[String] = { make_theory_content(name) orElse { try { Some(Line.normalize(File.read(node_file(name)))) } catch { case ERROR(_) => None } } } def get_file_content(name: Document.Node.Name): Option[String] = get_model(name) match { case Some(model) => Some(model.content.text) case None => read_file_content(name) } override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val file = node_file(name) get_model(file) match { case Some(model) => f(Scan.char_reader(model.content.text)) case None if file.isFile => using(Scan.byte_reader(file))(f) case None => error("No such file: " + quote(file.toString)) } } /* document models */ def visible_node(name: Document.Node.Name): Boolean = get_model(name) match { case Some(model) => model.node_visible case None => false } def change_model( session: Session, - editor: Server.Editor, + editor: Language_Server.Editor, file: JFile, version: Long, text: String, range: Option[Line.Range] = None) { 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)) }) } def close_model(file: JFile): Boolean = state.change_result(st => st.models.get(file) match { case None => (false, st) case Some(model) => (true, st.update_models(Some(file -> model.external(true)))) }) def sync_models(changed_files: Set[JFile]): Unit = state.change(st => { val changed_models = (for { (file, model) <- st.models.iterator if changed_files(file) && model.external_file text <- read_file_content(model.node_name) model1 <- model.change_text(text) } yield (file, model1)).toList st.update_models(changed_models) }) /* overlays */ def node_overlays(name: Document.Node.Name): Document.Node.Overlays = state.value.overlays(name) def insert_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) def remove_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) /* resolve dependencies */ def resolve_dependencies( session: Session, - editor: Server.Editor, + editor: Language_Server.Editor, file_watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => { /* theory files */ val thys = (for ((_, model) <- st.models.iterator if model.is_theory) yield (model.node_name, Position.none)).toList val thy_files1 = resources.dependencies(thys).theories val thy_files2 = (for { (_, model) <- st.models.iterator thy_name <- resources.make_theory_name(model.node_name) } yield thy_name).toList /* auxiliary files */ val stable_tip_version = if (st.models.forall(entry => entry._2.is_stable)) session.get_state().stable_tip_version else None val aux_files = stable_tip_version match { case Some(version) => undefined_blobs(version.nodes) case None => Nil } /* loaded models */ val loaded_models = (for { node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator file = node_file(node_name) if !st.models.isDefinedAt(file) 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 val invoke_input = loaded_models.nonEmpty val invoke_load = stable_tip_version.isEmpty ((invoke_input, invoke_load), st.update_models(loaded_models)) }) } /* pending input */ def flush_input(session: Session, channel: Channel) { state.change(st => { val changed_models = (for { file <- st.pending_input.iterator model <- st.models.get(file) (edits, model1) <- model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file)) } 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)) st.copy( models = st.models ++ changed_models.iterator.map(_._2), pending_input = Set.empty) }) } /* pending output */ def update_output(changed_nodes: Traversable[JFile]): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) def update_output_visible(): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ (for ((file, model) <- st.models.iterator if model.node_visible) yield file))) def flush_output(channel: Channel): Boolean = { state.change_result(st => { val (postponed, flushed) = (for { file <- st.pending_output.iterator model <- st.models.get(file) } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated) val changed_iterator = for { (file, model, rendering) <- flushed.iterator (changed_diags, changed_decos, model1) = model.publish(rendering) if changed_diags.isDefined || changed_decos.isDefined } 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)) } (file, model1) } (postponed.nonEmpty, st.copy( models = st.models ++ changed_iterator, pending_output = postponed.map(_._1).toSet)) } ) } /* output text */ def output_text(s: String): String = if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_xml(xml: XML.Tree): String = output_text(XML.content(xml)) def output_pretty(body: XML.Body, margin: Int): String = output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric)) def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) /* caret handling */ def update_caret(caret: Option[(JFile, Line.Position)]) { state.change(_.update_caret(caret)) } def get_caret(): Option[VSCode_Resources.Caret] = { val st = state.value for { (file, pos) <- st.caret model <- st.models.get(file) offset <- model.content.doc.offset(pos) } yield VSCode_Resources.Caret(file, model, offset) } /* spell checker */ val spell_checker = new Spell_Checker_Variable spell_checker.update(options) } diff --git a/src/Tools/VSCode/src/vscode_spell_checker.scala b/src/Tools/VSCode/src/vscode_spell_checker.scala --- a/src/Tools/VSCode/src/vscode_spell_checker.scala +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala @@ -1,73 +1,73 @@ /* Title: Tools/VSCode/src/vscode_spell_checker.scala Author: Makarius Specific spell-checker support for Isabelle/VSCode. */ package isabelle.vscode import isabelle._ 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 = (for { spell_checker <- rendering.resources.spell_checker.get.iterator spell <- rendering.spell_checker(model.content.text_range).iterator 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 { spell_checker <- rendering.resources.spell_checker.get range = rendering.before_caret_range(caret) Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) } yield (spell_checker, word) 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))), command = Some(command)) 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 + ")")) } update_items ::: reset_items case None => Nil } } }