equal
deleted
inserted
replaced
256 val process = |
256 val process = |
257 if (Sessions.is_pure(name)) { |
257 if (Sessions.is_pure(name)) { |
258 val eval = |
258 val eval = |
259 "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" + |
259 "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" + |
260 " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));" |
260 " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));" |
261 ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval), |
261 ML_Process(info.options, |
|
262 raw_ml_system = true, args = List("--use", "ROOT.ML", "--eval", eval), |
262 cwd = info.dir.file, env = env, tree = Some(tree), store = store) |
263 cwd = info.dir.file, env = env, tree = Some(tree), store = store) |
263 } |
264 } |
264 else { |
265 else { |
265 val args_file = Isabelle_System.tmp_file("build") |
266 val args_file = Isabelle_System.tmp_file("build") |
266 File.write(args_file, YXML.string_of_body( |
267 File.write(args_file, YXML.string_of_body( |