equal
deleted
inserted
replaced
72 def session_args(): String = |
72 def session_args(): String = |
73 { |
73 { |
74 val print_modes = |
74 val print_modes = |
75 (space_explode(',', PIDE.options.string("jedit_print_mode")) ::: |
75 (space_explode(',', PIDE.options.string("jedit_print_mode")) ::: |
76 space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _) |
76 space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _) |
77 (print_modes ::: List("-r", "-q", quote(session_name()))).mkString(" ") |
77 (print_modes ::: List("-r", "-q", File.shell_quote(session_name()))).mkString(" ") |
78 } |
78 } |
79 |
79 |
80 def session_start(): Unit = PIDE.session.start("Isabelle", session_args()) |
80 def session_start(): Unit = PIDE.session.start("Isabelle", session_args()) |
81 |
81 |
82 def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) |
82 def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) |