src/Tools/jEdit/src/jedit_sessions.scala
changeset 65254 3075aa3b40bf
parent 65252 8b776d12f6c0
child 65256 c3d6dd17d626
equal deleted inserted replaced
65253:85c0ac5c2589 65254:3075aa3b40bf
    81 
    81 
    82   def session_base(): Sessions.Base =
    82   def session_base(): Sessions.Base =
    83   {
    83   {
    84     val base =
    84     val base =
    85       try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
    85       try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
    86       catch { case ERROR(_) => Sessions.Base.empty }
    86       catch { case ERROR(_) => Sessions.pure_base(PIDE.options.value) }
    87     base.copy(known_theories =
    87     base.copy(known_theories =
    88       for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
    88       for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
    89   }
    89   }
    90 
    90 
    91 
    91