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