equal
deleted
inserted
replaced
133 def session_start(options: Options) |
133 def session_start(options: Options) |
134 { |
134 { |
135 Isabelle_Process.start(PIDE.session, session_options(options), |
135 Isabelle_Process.start(PIDE.session, session_options(options), |
136 sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure), |
136 sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure), |
137 logic = PIDE.resources.session_name, |
137 logic = PIDE.resources.session_name, |
138 store = Sessions.store(session_build_mode() == "system"), |
138 store = Some(Sessions.store(options, session_build_mode() == "system")), |
139 modes = |
139 modes = |
140 (space_explode(',', options.string("jedit_print_mode")) ::: |
140 (space_explode(',', options.string("jedit_print_mode")) ::: |
141 space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse, |
141 space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse, |
142 phase_changed = PIDE.plugin.session_phase_changed) |
142 phase_changed = PIDE.plugin.session_phase_changed) |
143 } |
143 } |