src/Tools/jEdit/src/jedit_sessions.scala
changeset 65572 6acb28e5ba41
parent 65571 923e32ad0976
child 66460 f7b0d6fb417a
     1.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:05:24 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:23:07 2017 +0200
     1.3 @@ -30,6 +30,9 @@
     1.4        case s => options.string("ML_process_policy") = s
     1.5      }
     1.6  
     1.7 +  def session_restricted(): Boolean =
     1.8 +    Isabelle_System.getenv("JEDIT_LOGIC_RESTRICT") == "true"
     1.9 +
    1.10    def session_info(options: Options): Info =
    1.11    {
    1.12      val logic =
    1.13 @@ -43,16 +46,19 @@
    1.14          catch { case ERROR(_) => None }
    1.15        info <- sessions.get(logic)
    1.16        parent <- info.parent
    1.17 -      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    1.18 +      if session_restricted()
    1.19      } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    1.20    }
    1.21  
    1.22    def session_name(options: Options): String = session_info(options).name
    1.23  
    1.24    def session_base(options: Options): Sessions.Base =
    1.25 +  {
    1.26 +    val all_known = !session_restricted()
    1.27      Sessions.session_base(
    1.28 -      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    1.29 +      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
    1.30      .platform_path
    1.31 +  }
    1.32  
    1.33    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    1.34