# HG changeset patch
# User wenzelm
# Date 1659609813 -7200
# Node ID a0253e471aa4185845090b5c76cb18be85a9187f
# Parent  204b97d05abe091fb003cde87f1504a4f2f56b61
clarified signature;

diff -r 204b97d05abe -r a0253e471aa4 src/Pure/PIDE/resources.scala
--- 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 */
 
diff -r 204b97d05abe -r a0253e471aa4 src/Tools/jEdit/src/jedit_sessions.scala
--- 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)
diff -r 204b97d05abe -r a0253e471aa4 src/Tools/jEdit/src/main_plugin.scala
--- 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
diff -r 204b97d05abe -r a0253e471aa4 src/Tools/jEdit/src/session_build.scala
--- 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)) }