--- 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,
--- 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,
--- 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)
+ }
+ })
}