src/Pure/Tools/build.scala
changeset 66712 4c98c929a12a
parent 66666 1a620647285c
child 66717 67dbf5cdc056
equal deleted inserted replaced
66711:80fa1401cf76 66712:4c98c929a12a
   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,