equal
deleted
inserted
replaced
9 |
9 |
10 object Other_Isabelle |
10 object Other_Isabelle |
11 { |
11 { |
12 def apply(isabelle_home: Path, |
12 def apply(isabelle_home: Path, |
13 isabelle_identifier: String = "", |
13 isabelle_identifier: String = "", |
14 user_home: Path = Path.explode("$USER_HOME"), |
14 user_home: Path = Path.USER_HOME, |
15 progress: Progress = new Progress): Other_Isabelle = |
15 progress: Progress = new Progress): Other_Isabelle = |
16 new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) |
16 new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) |
17 } |
17 } |
18 |
18 |
19 class Other_Isabelle( |
19 class Other_Isabelle( |