equal
deleted
inserted
replaced
47 } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none) |
47 } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none) |
48 } |
48 } |
49 |
49 |
50 def session_name(options: Options): String = session_info(options).name |
50 def session_name(options: Options): String = session_info(options).name |
51 |
51 |
52 def session_base(options: Options): (List[String], Sessions.Base) = |
52 def session_base_info(options: Options): Sessions.Base_Info = |
53 { |
53 { |
54 val (errs, base) = |
54 Sessions.session_base_info(options, |
55 Sessions.session_base_errors( |
55 session_name(options), |
56 options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true) |
56 dirs = JEdit_Sessions.session_dirs(), |
57 (errs, base.platform_path) |
57 all_known = true).platform_path |
58 } |
58 } |
59 |
59 |
60 def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE") |
60 def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE") |
61 |
61 |
62 def session_build( |
62 def session_build( |