equal
deleted
inserted
replaced
59 } |
59 } |
60 |
60 |
61 def session_args(): List[String] = |
61 def session_args(): List[String] = |
62 { |
62 { |
63 val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) |
63 val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) |
64 modes ::: List(jedit_logic()) |
64 modes ::: List("-r", "-q", jedit_logic()) |
65 } |
65 } |
66 |
66 |
67 def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) |
67 def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) |
68 |
68 |
69 def session_list(): List[String] = |
69 def session_list(): List[String] = |