equal
deleted
inserted
replaced
24 if (changed.isEmpty) None |
24 if (changed.isEmpty) None |
25 else |
25 else |
26 Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2) |
26 Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2) |
27 .mkString("\n")) |
27 .mkString("\n")) |
28 |
28 |
29 def change(path: Path) |
29 def change(path: Path): Unit = |
30 { |
30 { |
31 def change_line(line: String, entry: (String, String)): String = |
31 def change_line(line: String, entry: (String, String)): String = |
32 line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) |
32 line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) |
33 File.change(path, s => |
33 File.change(path, s => |
34 split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n")) |
34 split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n")) |
54 def build_csdp( |
54 def build_csdp( |
55 download_url: String = default_download_url, |
55 download_url: String = default_download_url, |
56 verbose: Boolean = false, |
56 verbose: Boolean = false, |
57 progress: Progress = new Progress, |
57 progress: Progress = new Progress, |
58 target_dir: Path = Path.current, |
58 target_dir: Path = Path.current, |
59 mingw: MinGW = MinGW.none) |
59 mingw: MinGW = MinGW.none): Unit = |
60 { |
60 { |
61 mingw.check |
61 mingw.check |
62 |
62 |
63 Isabelle_System.with_tmp_dir("build")(tmp_dir => |
63 Isabelle_System.with_tmp_dir("build")(tmp_dir => |
64 { |
64 { |