src/Pure/System/build.ML
changeset 48804 6348e5fca42e
parent 48734 af91cd2301ba
child 48805 c3ea910b3581
equal deleted inserted replaced
48795:bece259ee055 48804:6348e5fca42e
    63           let open XML.Decode in
    63           let open XML.Decode in
    64             pair bool (pair Options.decode (pair bool (pair string (pair string
    64             pair bool (pair Options.decode (pair bool (pair string (pair string
    65               (pair string ((list (pair Options.decode (list string)))))))))
    65               (pair string ((list (pair Options.decode (list string)))))))))
    66           end;
    66           end;
    67 
    67 
       
    68       val document_variants =
       
    69         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    68       val _ =
    70       val _ =
    69         Session.init do_output false
    71         Session.init do_output false
    70           (Options.bool options "browser_info") browser_info
    72           (Options.bool options "browser_info") browser_info
    71           (Options.string options "document")
    73           (Options.string options "document")
    72           (Options.bool options "document_graph")
    74           (Options.bool options "document_graph")
    73           (space_explode ":" (Options.string options "document_variants"))
    75           document_variants
    74           parent_name name
    76           parent_name name
    75           (Options.string options "document_dump",
    77           (Options.string options "document_dump",
    76             Present.dump_mode (Options.string options "document_dump_mode"))
    78             Present.dump_mode (Options.string options "document_dump_mode"))
    77           "" verbose;
    79           "" verbose;
    78       val _ =
    80       val _ =