equal
deleted
inserted
replaced
40 Standard_System.with_tmp_file("settings") { dump => |
40 Standard_System.with_tmp_file("settings") { dump => |
41 val shell_prefix = |
41 val shell_prefix = |
42 if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil |
42 if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil |
43 val cmdline = |
43 val cmdline = |
44 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) |
44 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) |
45 val (output, rc) = |
45 val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*) |
46 Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*)) |
|
47 if (rc != 0) error(output) |
46 if (rc != 0) error(output) |
48 |
47 |
49 val entries = |
48 val entries = |
50 for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield { |
49 for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield { |
51 val i = entry.indexOf('=') |
50 val i = entry.indexOf('=') |