# HG changeset patch # User wenzelm # Date 1761951897 -3600 # Node ID 5c70d1c27a2e73cd3db8ad74fd05cdb56fba0f8c # Parent e26f102d2498a24fcb0b35d65d160991202711ec clarified modules; diff -r e26f102d2498 -r 5c70d1c27a2e src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Oct 31 18:21:34 2025 +0100 +++ b/src/Pure/System/isabelle_tool.scala Sat Nov 01 00:04:57 2025 +0100 @@ -163,8 +163,8 @@ Update_Theorems.isabelle_tool, Update_Tool.isabelle_tool, isabelle.mirabelle.Mirabelle.isabelle_tool, - isabelle.vscode.Language_Server.isabelle_tool, - isabelle.vscode.VSCode_Main.isabelle_tool) + isabelle.vscode.VSCode_Main.isabelle_tool1, + isabelle.vscode.VSCode_Main.isabelle_tool2) class Admin_Tools extends Isabelle_Scala_Tools( Build_Doc.isabelle_tool, diff -r e26f102d2498 -r 5c70d1c27a2e src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Fri Oct 31 18:21:34 2025 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Sat Nov 01 00:04:57 2025 +0100 @@ -13,7 +13,7 @@ import isabelle._ -import java.io.{PrintStream, OutputStream, File => JFile} +import java.io.{File => JFile} import scala.collection.mutable import scala.annotation.tailrec @@ -21,87 +21,12 @@ 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", Scala_Project.here, - { args => - try { - var logic_ancestor: Option[String] = None - var log_file: Option[Path] = None - var logic_requirements = false - val dirs = new mutable.ListBuffer[Path] - val include_sessions = new mutable.ListBuffer[String] - var logic = default_logic - var modes: List[String] = Nil - var no_build = false - 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 - -n no build of session image on startup - -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 += Path.explode(File.standard_path(arg))), - "i:" -> (arg => include_sessions += arg), - "l:" -> (arg => logic = arg), - "m:" -> (arg => modes = arg :: modes), - "n" -> (_ => no_build = true), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose = true)) - - val more_args = getopts(args) - if (more_args.nonEmpty) getopts.usage() - - val log = Logger.make_file(log_file) - val channel = new Channel(System.in, System.out, log, verbose) - val server = - new Language_Server(channel, options, session_name = logic, session_dirs = dirs.toList, - include_sessions = include_sessions.toList, session_ancestor = logic_ancestor, - session_requirements = logic_requirements, session_no_build = no_build, - modes = modes, log = log) - - // prevent spurious garbage on the main protocol channel - val orig_out = System.out - try { - System.setOut(new PrintStream(OutputStream.nullOutputStream())) - server.start() - } - finally { System.setOut(orig_out) } - } - catch { - case exn: Throwable => - val channel = new Channel(System.in, System.out, new Logger) - channel.error_message(Exn.message(exn)) - throw(exn) - } - }) } class Language_Server( val channel: Channel, val options: Options, - session_name: String = Language_Server.default_logic, + session_name: String = Isabelle_System.getenv("ISABELLE_LOGIC"), include_sessions: List[String] = Nil, session_dirs: List[Path] = Nil, session_ancestor: Option[String] = None, diff -r e26f102d2498 -r 5c70d1c27a2e src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Fri Oct 31 18:21:34 2025 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Sat Nov 01 00:04:57 2025 +0100 @@ -10,6 +10,7 @@ import isabelle._ import java.util.zip.ZipFile +import java.io.{PrintStream, OutputStream} import scala.collection.mutable @@ -169,9 +170,9 @@ } - /* Isabelle tool wrapper */ + /* Isabelle tool wrappers */ - val isabelle_tool = + val isabelle_tool1 = Isabelle_Tool("vscode", "Isabelle/VSCode interface wrapper", Scala_Project.here, { args => var logic_ancestor = "" @@ -255,4 +256,78 @@ server_log = server_log, verbose = verbose, background = background, progress = app_progress).check }) + + + /* Isabelle tool wrapper */ + + val isabelle_tool2 = + Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", Scala_Project.here, + { args => + try { + var logic_ancestor: Option[String] = None + var log_file: Option[Path] = None + var logic_requirements = false + val dirs = new mutable.ListBuffer[Path] + val include_sessions = new mutable.ListBuffer[String] + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var modes: List[String] = Nil + var no_build = false + 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(Isabelle_System.getenv("ISABELLE_LOGIC")) + """) + -m MODE add print mode for output + -n no build of session image on startup + -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 += Path.explode(File.standard_path(arg))), + "i:" -> (arg => include_sessions += arg), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "n" -> (_ => no_build = true), + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose = true)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val log = Logger.make_file(log_file) + val channel = new Channel(System.in, System.out, log, verbose) + val server = + new Language_Server(channel, options, session_name = logic, session_dirs = dirs.toList, + include_sessions = include_sessions.toList, session_ancestor = logic_ancestor, + session_requirements = logic_requirements, session_no_build = no_build, + modes = modes, log = log) + + // prevent spurious garbage on the main protocol channel + val orig_out = System.out + try { + System.setOut(new PrintStream(OutputStream.nullOutputStream())) + server.start() + } + finally { System.setOut(orig_out) } + } + catch { + case exn: Throwable => + val channel = new Channel(System.in, System.out, new Logger) + channel.error_message(Exn.message(exn)) + throw(exn) + } + }) }