equal
deleted
inserted
replaced
113 (path ()) name doc_dump (get_rpath rpath) verbose |
113 (path ()) name doc_dump (get_rpath rpath) verbose |
114 (map Thy_Info.get_theory (Thy_Info.get_names ()))); |
114 (map Thy_Info.get_theory (Thy_Info.get_names ()))); |
115 |
115 |
116 local |
116 local |
117 |
117 |
118 fun doc_dump (cp, dump) = (if cp then "all" else "tex+sty", dump); |
118 fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty"); |
119 |
119 |
120 in |
120 in |
121 |
121 |
122 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
122 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
123 name dump rpath level timing verbose max_threads trace_threads |
123 name dump rpath level timing verbose max_threads trace_threads |