588 (command_timings, (do_output, (info.options, (verbose, (browser_info, |
588 (command_timings, (do_output, (info.options, (verbose, (browser_info, |
589 (info.document_files, (Isabelle_System.posix_path(graph_file), (parent, |
589 (info.document_files, (Isabelle_System.posix_path(graph_file), (parent, |
590 (info.chapter, (name, theories))))))))))) |
590 (info.chapter, (name, theories))))))))))) |
591 })) |
591 })) |
592 |
592 |
593 private val env = |
593 private val env0 = |
594 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output), |
594 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output), |
595 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |
595 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |
596 Isabelle_System.posix_path(args_file)) |
596 Isabelle_System.posix_path(args_file)) |
|
597 |
|
598 private val env = |
|
599 if (is_pure(name)) |
|
600 env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) |
|
601 else env0 |
597 |
602 |
598 private val script = |
603 private val script = |
599 if (is_pure(name)) { |
604 if (is_pure(name)) { |
600 if (do_output) "./build " + name + " \"$OUTPUT\"" |
605 if (do_output) "./build " + name + " \"$OUTPUT\"" |
601 else """ rm -f "$OUTPUT"; ./build """ + name |
606 else """ rm -f "$OUTPUT"; ./build """ + name |