equal
deleted
inserted
replaced
104 |
104 |
105 /* session build process */ |
105 /* session build process */ |
106 |
106 |
107 def session_base_info(options: Options): Sessions.Base_Info = |
107 def session_base_info(options: Options): Sessions.Base_Info = |
108 Sessions.base_info(options, |
108 Sessions.base_info(options, |
|
109 dirs = JEdit_Sessions.session_dirs(), |
109 session = |
110 session = |
110 if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options) |
111 if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options) |
111 else logic_name(options), |
112 else logic_name(options), |
112 dirs = JEdit_Sessions.session_dirs(), |
|
113 ancestor_session = logic_ancestor, |
113 ancestor_session = logic_ancestor, |
114 all_known = !logic_focus, |
114 all_known = !logic_focus, |
115 focus_session = logic_focus, |
115 focus_session = logic_focus, |
116 required_session = logic_base) |
116 required_session = logic_base) |
117 |
117 |