Permalink
Fetching contributors…
Cannot retrieve contributors at this time
202 lines (171 sloc) 6.92 KB
val _ = quietdec := true;
(* ----------------------------------------------------------------------
Establish the basic environment and bring in the HOL kernel
---------------------------------------------------------------------- *)
load "PP";
structure MosmlPP = PP
(* ----------------------------------------------------------------------
Set interactive flag to true
---------------------------------------------------------------------- *)
val _ = load "Globals";
val _ = Globals.interactive := true;
val _ = app load
["Mosml", "Process", "Path", "boolLib", "proofManagerLib", "Arbrat"];
open HolKernel Parse boolLib proofManagerLib;
(* Loading HolKernel installs the "standard" set of infixes, which are
set up in src/0/Overlay.sml *)
(*---------------------------------------------------------------------------*
* Install prettyprinters *
*---------------------------------------------------------------------------*)
local
fun pp_from_stringfn sf pps x = PP.add_string pps (sf x)
fun gprint g pps t = let
val tyg = Parse.type_grammar()
val (_, ppt) = Parse.print_from_grammars (tyg,g)
in
ppt pps t
end
fun ppg pps g = term_grammar.prettyprint_grammar gprint pps g
fun ppgrules pps grs = term_grammar.prettyprint_grammar_rules gprint pps grs
fun timepp pps t = PP.add_string pps (Time.toString t ^ "s")
fun locpp pps l = PP.add_string pps (locn.toShortString l)
structure MPP = MosmlPP
in
fun mosmlpp ppfn pps x = let
val slist = ref ([] : string list)
fun output_slist () = (app (MPP.add_string pps) (List.rev (!slist));
slist := [])
fun flush ()= output_slist()
fun consume_string s = let
open Substring
val (pfx,sfx) = splitl (fn c => c <> #"\n") (full s)
in
if size sfx = 0 then slist := s :: !slist
else
(output_slist();
MPP.add_newline pps;
if size sfx > 1 then consume_string (string (triml 1 sfx))
else ())
end
val consumer = {consumer = consume_string,
linewidth = !Globals.linewidth,
flush = flush}
val newpps = HOLPP.mk_ppstream consumer
in
MPP.begin_block pps MPP.INCONSISTENT 0;
HOLPP.begin_block newpps HOLPP.INCONSISTENT 0;
ppfn newpps x;
HOLPP.end_block newpps;
HOLPP.flush_ppstream newpps;
MPP.end_block pps
end
val _ = installPP (mosmlpp Pretype.pp_pretype)
val _ = installPP (mosmlpp (Parse.term_pp_with_delimiters Hol_pp.pp_term))
val _ = installPP (mosmlpp (Parse.type_pp_with_delimiters Hol_pp.pp_type))
val _ = installPP (mosmlpp Hol_pp.pp_thm)
val _ = installPP (mosmlpp Hol_pp.pp_theory)
val _ = installPP (mosmlpp type_grammar.prettyprint_grammar)
val _ = installPP (mosmlpp ppg)
val _ = installPP (mosmlpp ppgrules)
val _ = installPP (mosmlpp proofManagerLib.pp_proof)
val _ = installPP (mosmlpp proofManagerLib.pp_proofs)
val _ = installPP (mosmlpp Rewrite.pp_rewrites)
val _ = installPP (mosmlpp TypeBasePure.pp_tyinfo)
val _ = installPP (mosmlpp DefnBase.pp_defn)
val _ = installPP (mosmlpp Arbnum.pp_num)
val _ = installPP (mosmlpp Arbint.pp_int)
val _ = installPP (mosmlpp Arbrat.pp_rat)
val _ = installPP (mosmlpp timepp)
val _ = installPP (mosmlpp locpp)
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/HOL.help",
term = "hol", title = "HOL 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
(*---------------------------------------------------------------------------*
* 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 exit_string =
if Systeml.OS = "winNT" then
"To exit type <Control>-Z <Return> (*not* quit();)"
else
"To exit type <Control>-D (*not* quit();)"
(* ----------------------------------------------------------------------
if present, look at a Holmakefile in the current directory to see
if we should extend the loadPath
---------------------------------------------------------------------- *)
structure HOL_Interactive : sig
val toggle_quietdec : unit -> bool
val amquiet : unit -> bool
val print_banner : unit -> unit
end =
struct
fun toggle_quietdec () = (Meta.quietdec := not (!Meta.quietdec) ;
!Meta.quietdec)
fun amquiet () = !Meta.quietdec
fun print_banner() =
TextIO.output(TextIO.stdOut,
"\n---------------------------------------------------------------------\n"
^" HOL-4 ["
^Globals.release^" "^Lib.int_to_string(Globals.version)
^" ("^Thm.kernelid^", "^build_stamp
^")]\n\n"
^" For introductory HOL help, type: help \"hol\";\n"
^" "^exit_string
^"\n---------------------------------------------------------------------\
\\n\n")
end;
val _ = HOL_Interactive.print_banner()
local
open Path
in
val _ = loadPath := concat (HOLDIR, concat ("tools", "Holmake")) :: !loadPath
val _ = load "ReadHMF.uo"
val _ = loadPath := tl (!loadPath)
end;
use (OS.Path.concat (HOLDIR, OS.Path.concat("tools", "makefile-includes.ML")));
use (Path.concat(Globals.HOLDIR, "tools/check-intconfig.sml"));
(* Local variables: *)
(* mode: sml *)
(* end: *)