207 import XML.Encode._ |
207 import XML.Encode._ |
208 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, |
208 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, |
209 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, |
209 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, |
210 pair(string, pair(string, pair(string, pair(Path.encode, |
210 pair(string, pair(string, pair(string, pair(Path.encode, |
211 pair(list(pair(Options.encode, list(pair(string, properties)))), |
211 pair(list(pair(Options.encode, list(pair(string, properties)))), |
212 pair(list(pair(string, string)), pair(list(pair(string, string)), |
212 pair(list(pair(string, string)), pair(list(string), |
213 list(pair(string, string))))))))))))))))( |
213 list(pair(string, string))))))))))))))))( |
214 (Symbol.codes, (command_timings, (do_output, (verbose, |
214 (Symbol.codes, (command_timings, (do_output, (verbose, |
215 (store.browser_info, (info.document_files, (File.standard_path(graph_file), |
215 (store.browser_info, (info.document_files, (File.standard_path(graph_file), |
216 (parent, (info.chapter, (name, (Path.current, |
216 (parent, (info.chapter, (name, (Path.current, |
217 (info.theories, |
217 (info.theories, |