551 if (is_pure(name)) Options.encode(info.options) |
551 if (is_pure(name)) Options.encode(info.options) |
552 else |
552 else |
553 { |
553 { |
554 val theories = info.theories.map(x => (x._2, x._3)) |
554 val theories = info.theories.map(x => (x._2, x._3)) |
555 import XML.Encode._ |
555 import XML.Encode._ |
556 pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, |
556 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode, |
557 pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, |
557 pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, |
558 pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))( |
558 pair(string, pair(string, pair(string, |
559 (command_timings, (do_output, (info.options, (verbose, (browser_info, |
559 list(pair(Options.encode, list(Path.encode))))))))))))))( |
560 (info.document_files, (File.standard_path(graph_file), (parent, |
560 (Symbol.codes, (command_timings, (do_output, (info.options, |
561 (info.chapter, (name, theories))))))))))) |
561 (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file), |
|
562 (parent, (info.chapter, (name, |
|
563 theories)))))))))))) |
562 })) |
564 })) |
563 |
565 |
564 private val env = |
566 private val env = |
565 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output), |
567 Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output), |
566 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |
568 (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> |