more uniform session_system_mode (see also e57416b649d5);
authorwenzelm
Fri, 01 Mar 2019 20:16:26 +0100
changeset 69853 f7c9a1be333f
parent 69852 54243334edcf
child 69854 cc0b3e177b49
more uniform session_system_mode (see also e57416b649d5);
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 01 17:00:55 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 01 20:16:26 2019 +0100
@@ -29,6 +29,9 @@
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
+  def session_system_mode(): Boolean =
+    session_build_mode() match { case "" | "system" => true case _ => false }
+
   def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
     Sessions.load_structure(session_options(options), dirs = dirs)
 
@@ -119,10 +122,8 @@
   def session_build(
     options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
   {
-    val mode = session_build_mode()
-
     Build.build(session_options(options), progress = progress, build_heap = true,
-      no_build = no_build, system_mode = mode == "" || mode == "system",
+      no_build = no_build, system_mode = session_system_mode(),
       dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
       sessions = List(PIDE.resources.session_name)).rc
   }
@@ -132,7 +133,7 @@
     Isabelle_Process.start(PIDE.session, session_options(options),
       sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
       logic = PIDE.resources.session_name,
-      store = Some(Sessions.store(options, session_build_mode() == "system")),
+      store = Some(Sessions.store(options, session_system_mode())),
       modes =
         (space_explode(',', options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,