--- a/src/Pure/PIDE/resources.scala Thu Aug 04 12:14:56 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Thu Aug 04 12:43:33 2022 +0200
@@ -34,8 +34,6 @@
) {
resources =>
- def session_name: String = session_base.session_name
-
/* init session */
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Aug 04 12:14:56 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Aug 04 12:43:33 2022 +0200
@@ -125,7 +125,7 @@
no_build: Boolean = false
): Int = {
Build.build(session_options(options),
- selection = Sessions.Selection.session(PIDE.resources.session_name),
+ selection = Sessions.Selection.session(PIDE.resources.session_base.session_name),
progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
infos = PIDE.resources.session_base_info.infos).rc
}
@@ -139,7 +139,7 @@
session.phase_changed += PIDE.plugin.session_phase_changed
Isabelle_Process.start(session, options, sessions_structure, store,
- logic = PIDE.resources.session_name,
+ logic = PIDE.resources.session_base.session_name,
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
--- a/src/Tools/jEdit/src/main_plugin.scala Thu Aug 04 12:14:56 2022 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala Thu Aug 04 12:43:33 2022 +0200
@@ -284,7 +284,7 @@
private def init_title(view: View): Unit = {
val title =
proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
- "/" + PIDE.resources.session_name
+ "/" + PIDE.resources.session_base.session_name
val marker = "\u200B"
val old_title = view.getViewConfig.title
--- a/src/Tools/jEdit/src/session_build.scala Thu Aug 04 12:14:56 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Thu Aug 04 12:43:33 2022 +0200
@@ -155,7 +155,8 @@
setVisible(true)
Isabelle_Thread.fork(name = "session_build") {
- progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
+ progress.echo("Build started for Isabelle/" +
+ PIDE.resources.session_base.session_name + " ...")
val (out, rc) =
try { ("", JEdit_Sessions.session_build(options, progress = progress)) }