equal
deleted
inserted
replaced
80 } |
80 } |
81 |
81 |
82 def session_base(): Sessions.Base = |
82 def session_base(): Sessions.Base = |
83 { |
83 { |
84 val base = |
84 val base = |
85 try { Build.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.Base.empty } |
87 base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_)))) |
87 base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_)))) |
88 } |
88 } |
89 |
89 |
90 |
90 |