equal
deleted
inserted
replaced
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.explode("$USER_HOME"), |
15 progress: Progress = No_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( |
20 val isabelle_home: Path, |
20 val isabelle_home: Path, |