val _ = quietdec := true;


(* ----------------------------------------------------------------------
    Establish the basic environment and bring in the HOL kernel
   ---------------------------------------------------------------------- *)

val _ = app load
  ["Mosml", "Process", "Path", "boolLib", "goalstackLib", "Arbint"];

open HolKernel Parse boolLib goalstackLib;

(* Loading HolKernel installs the "standard" set of infixes, which are
   set up in src/0/Overlay.sml *)

(*---------------------------------------------------------------------------*
 *   Install prettyprinters                                                  *
 *---------------------------------------------------------------------------*)

local
  fun with_pp ppfn pps x =
      Parse.respect_width_ref Globals.linewidth ppfn pps x handle e => Raise e
  fun pp_from_stringfn sf pps x = PP.add_string pps (sf x)
in
  val _ = installPP (with_pp (Parse.term_pp_with_delimiters Hol_pp.pp_term))
  val _ = installPP (with_pp (Parse.type_pp_with_delimiters Hol_pp.pp_type))
  val _ = installPP (with_pp Hol_pp.pp_thm)
  val _ = installPP (with_pp Hol_pp.pp_theory)
  val _ = installPP (with_pp type_grammar.prettyprint_grammar)
  val _ = installPP (with_pp term_grammar.prettyprint_grammar)

  val _ = installPP (with_pp goalstackLib.pp_proofs)
  val _ = installPP (with_pp goalstackLib.pp_goalstack)
  val _ = installPP (with_pp Rewrite.pp_rewrites)
  val _ = installPP (with_pp TypeBasePure.pp_tyinfo)
  val _ = installPP (with_pp DefnBase.pp_defn)
  val _ = installPP (with_pp Arbnum.pp_num)
  val _ = installPP (with_pp Arbint.pp_int)
end;


(*---------------------------------------------------------------------------*
 * Set up the help paths.                                                    *
 *---------------------------------------------------------------------------*)

local
  open Path
  fun HELP s = toString(fromString(concat(HOLDIR, concat("help",s))))
  val SIGOBJ = toString(fromString(concat(HOLDIR, "sigobj")))
in
  val () = indexfiles := HELP "HOL.Help" :: !indexfiles
  val () = helpdirs   := HOLDIR :: SIGOBJ :: !helpdirs
  val () = Help.specialfiles :=
             {file = "help/Docfiles/README.Hol98",
              term = "hol", title = "Hol98 Overview"}
             :: !Help.specialfiles
end


(*---------------------------------------------------------------------------*
 *  Set parameters for parsing and help.                                     *
 *---------------------------------------------------------------------------*)

val _ = quotation := true
val _ = Help.displayLines := 60;

(*---------------------------------------------------------------------------*
 *  Set up compile_theory function                                           *
 *---------------------------------------------------------------------------*)

fun compile_theory () = let
  val name = current_theory()
  val signame = name^"Theory.sig"
  val smlname = name^"Theory.sml"
  fun readable f = FileSys.access(f, [FileSys.A_READ])
in
  if readable signame andalso readable smlname then let
  in
     Meta.compileStructure ["Overlay"] signame;
     Meta.compileStructure ["Overlay"] smlname;
     print ("Compiled "^name^" theory files.\n")
  end
  else
     print "No theory files on disk; perhaps export_theory() required.\n"
end

(* ----------------------------------------------------------------------
    Set interactive flag to true
   ---------------------------------------------------------------------- *)

val _ = Globals.interactive := true;

(*---------------------------------------------------------------------------*
 * Print a banner.                                                           *
 *---------------------------------------------------------------------------*)

val build_stamp =
 let open TextIO Path
     val stampstr = openIn (concat(HOLDIR, concat("tools", "build-stamp")))
     val stamp = inputAll stampstr before closeIn stampstr
 in
     stamp
 end handle _ => "";

val _ =
TextIO.output(TextIO.stdOut,
  "\n-----------------------------------------------------------------\n"
  ^"       HOL-4 ["
  ^Globals.release^" "^Lib.int_to_string(Globals.version)^build_stamp
  ^"]\n\n       For introductory HOL help, type: help \"hol\";\n"
  ^"-----------------------------------------------------------------\n\n");

(* Local variables: *)
(* mode: sml *)
(* end: *)