1let 2 val s = "[loading theories and proof tools " 3 val l = ["optionTheory", "pairLib", "sumTheory", "numTheory", 4 "arithmeticTheory", "Arith", "numLib", "mesonLib", "BasicProvers", 5 "Datatype", "listTheory", "bossLib", "EmitTeX", "pred_setLib" 6 ] 7 val terminfo = case Process.getEnv "TERM" of 8 SOME s => s 9 | NONE => "" 10 val (prelude, dotchar) = 11 if terminfo <> "emacs" andalso terminfo <> "dumb" 12 then 13 (String.map (K #" ") s ^ 14 CharVector.tabulate(length l, K #"-") ^ " ]\r", "*") 15 else ("", ".") 16 fun dotload f = (print dotchar; load f) 17 val curdir = FileSys.getDir() 18 val () = FileSys.chDir (Path.concat(HOLDIR,"sigobj")) 19in 20 print prelude; 21 print s; 22 app dotload l; 23 print " ]\n"; 24 FileSys.chDir curdir 25end; 26 27val _ = installPP (mosmlpp simpLib.pp_ssfrag); 28val _ = installPP (mosmlpp simpLib.pp_simpset) 29val _ = installPP (mosmlpp DefnBase.pp_defn) 30 31open bossLib; (* Any others? *) 32 33val _ = use (HOLDIR^"/src/proofman/expandq"); 34(* val _ = use (HOLDIR^"/src/datatype/Interactive"); *) 35 36val _ = quietdec := false; 37