1val _ = use "../../tools-poly/poly/Binarymap.sig"; 2val _ = use "../../tools-poly/poly/Binarymap.sml"; 3val _ = use "../../tools-poly/poly/Binaryset.sig"; 4val _ = use "../../tools-poly/poly/Binaryset.sml"; 5val _ = use "../../tools-poly/poly/Listsort.sig"; 6val _ = use "../../tools-poly/poly/Listsort.sml"; 7 8fun useB f = 9 (use (f ^ ".sig"); 10 use (f ^ ".sml")); 11 12val _ = useB "Database"; 13val _ = use "HOLPage.sml"; 14val _ = useB "Htmlsigs"; 15val _ = use "Keepers.sml"; 16val _ = use "Asynt.sml"; 17 18fun u f = use ("../../tools/mlyacc/mlyacclib/" ^ f ^ ".sml"); 19val _ = u "MLY_base-sig"; 20val _ = u "MLY_join"; 21val _ = u "MLY_lrtable"; 22val _ = u "MLY_stream"; 23val _ = u "MLY_parser2"; 24 25 26val _ = useB "Parser.grm"; 27 28(* I think there's a bug in the lexer generator, but I don't want to fix it 29 * beause I don't know if that will break it on mosml. CharVector.foldl is used 30 * only for lexers with %count *) 31 32structure CharVector = struct 33open CharVector 34fun foldl f b vs = 35 CharVectorSlice.foldli f b (CharVectorSlice.slice vs) 36end; 37 38val _ = use "Lexer.lex.sml"; 39val _ = use "Parsspec.sml"; 40val _ = use "Printbase.sml"; 41val _ = useB "Symbolic"; 42 43val _ = useB "../../sigobj/Systeml"; 44 45val _ = use "makebase.sml"; 46 47val main = makebase.main 48