--- a/src/Pure/PIDE/headless.scala Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/PIDE/headless.scala Sat Aug 20 13:35:17 2022 +0200
@@ -565,11 +565,12 @@
print_mode: List[String] = Nil,
progress: Progress = new Progress
): Session = {
- val session = new Session(session_base_info.session, options, resources)
+ val session_name = session_base_info.session_name
+ val session = new Session(session_name, options, resources)
- progress.echo("Starting session " + session_base_info.session + " ...")
+ progress.echo("Starting session " + session_name + " ...")
Isabelle_Process.start(session, options, session_base_info.sessions_structure, store,
- logic = session_base_info.session, modes = print_mode).await_startup()
+ logic = session_name, modes = print_mode).await_startup()
session
}
--- a/src/Pure/Thy/export.scala Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/Thy/export.scala Sat Aug 20 13:35:17 2022 +0200
@@ -294,7 +294,7 @@
document_snapshot: Option[Document.Snapshot] = None,
close_database_context: Boolean = false
): Session_Context = {
- val session_name = session_base_info.check_errors.base.session_name
+ val session_name = session_base_info.check_errors.session_name
val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
val session_databases =
database_server match {
--- a/src/Pure/Thy/sessions.scala Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Aug 20 13:35:17 2022 +0200
@@ -364,7 +364,7 @@
errors: List[String] = Nil,
infos: List[Info] = Nil
) {
- def session: String = base.session_name
+ def session_name: String = base.session_name
def check_errors: Base_Info =
if (errors.isEmpty) this
--- a/src/Tools/VSCode/src/language_server.scala Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Sat Aug 20 13:35:17 2022 +0200
@@ -267,11 +267,11 @@
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)
+ selection = Sessions.Selection.session(base_info.session_name),
+ build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
if (!session_no_build && !build(no_build = true).ok) {
- val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
+ val start_msg = "Build started for Isabelle/" + base_info.session_name + " ..."
val fail_msg = "Session build failed -- prover process remains inactive!"
val progress = channel.progress(verbose = true)
@@ -304,8 +304,8 @@
try {
Isabelle_Process.start(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 + Isabelle_System.isabelle_heading())
+ Sessions.store(options), modes = modes, logic = base_info.session_name).await_startup()
+ reply_ok("Welcome to Isabelle/" + base_info.session_name + Isabelle_System.isabelle_heading())
}
catch { case ERROR(msg) => reply_error(msg) }
}