1val _ = quietdec := true;
2
3(* ----------------------------------------------------------------------
4    Establish the basic environment and bring in the HOL kernel
5   ---------------------------------------------------------------------- *)
6load "PP";
7structure MosmlPP = PP
8
9(* ----------------------------------------------------------------------
10    Set interactive flag to true
11   ---------------------------------------------------------------------- *)
12
13val _ = load "Globals";
14val _ = Globals.interactive := true;
15
16val _ = app load
17  ["Mosml", "Process", "Path", "boolLib", "proofManagerLib", "Arbrat"];
18
19open HolKernel Parse boolLib proofManagerLib;
20
21(* Loading HolKernel installs the "standard" set of infixes, which are
22   set up in src/0/Overlay.sml *)
23
24(*---------------------------------------------------------------------------*
25 *   Install prettyprinters                                                  *
26 *---------------------------------------------------------------------------*)
27
28local
29  fun pp_from_stringfn sf pps x = PP.add_string (sf x)
30  fun gprint0 g t = let
31    val tyg = Parse.type_grammar()
32    val (_, ppt) = Parse.print_from_grammars (tyg,g)
33  in
34    ppt t
35  end
36  val gprint = (fn g => fn t => smpp.lift (gprint0 g) t)
37  fun ppg g = Parse.mlower (term_grammar.prettyprint_grammar gprint g)
38  fun ppgrules grs =
39    Parse.mlower (term_grammar.prettyprint_grammar_rules gprint grs)
40  fun timepp t = PP.add_string (Time.toString t ^ "s")
41  fun locpp l = PP.add_string (locn.toShortString l)
42  structure MPP = MosmlPP
43  open PrettyImpl
44in
45  fun mosmlpp ppfn pps x = let
46    val slist = ref ([] : string list)
47    fun output_slist () = (app (MPP.add_string pps) (List.rev (!slist));
48                           slist := [])
49    fun consume_string s = let
50      open Substring
51      val (pfx,sfx) = splitl (fn c => c <> #"\n") (full s)
52    in
53      if size sfx = 0 then slist := s :: !slist
54      else
55        (output_slist();
56         MPP.add_newline pps;
57         if size sfx > 1 then consume_string (string (triml 1 sfx))
58         else ())
59    end
60  in
61    MPP.begin_block pps MPP.INCONSISTENT 0;
62    HOLPP.prettyPrint(consume_string, !Globals.linewidth) (ppfn x);
63    MPP.end_block pps;
64    output_slist()
65  end
66  val _ = installPP (mosmlpp Pretype.pp_pretype)
67  val _ = installPP (mosmlpp (Parse.term_pp_with_delimiters Hol_pp.pp_term))
68  val _ = installPP (mosmlpp (Parse.type_pp_with_delimiters Hol_pp.pp_type))
69  val _ = installPP (mosmlpp Hol_pp.pp_thm)
70  val _ = installPP (mosmlpp Hol_pp.pp_theory)
71  val _ = installPP (mosmlpp type_grammar.prettyprint_grammar)
72  val _ = installPP (mosmlpp ppg)
73  val _ = installPP (mosmlpp ppgrules)
74  val _ = installPP (mosmlpp proofManagerLib.pp_proof)
75  val _ = installPP (mosmlpp proofManagerLib.pp_proofs)
76  val _ = installPP (mosmlpp Rewrite.pp_rewrites)
77  val _ = installPP (mosmlpp TypeBasePure.pp_tyinfo)
78  val _ = installPP (mosmlpp Arbnum.pp_num)
79  val _ = installPP (mosmlpp Arbint.pp_int)
80  val _ = installPP (mosmlpp Arbrat.pp_rat)
81  val _ = installPP (mosmlpp timepp)
82  val _ = installPP (mosmlpp locpp)
83end;
84
85
86(*---------------------------------------------------------------------------*
87 * Set up the help paths.                                                    *
88 *---------------------------------------------------------------------------*)
89
90local
91  open Path
92  fun HELP s = toString(fromString(concat(HOLDIR, concat("help",s))))
93  val SIGOBJ = toString(fromString(concat(HOLDIR, "sigobj")))
94in
95  val () = indexfiles := HELP "HOL.Help" :: !indexfiles
96  val () = helpdirs   := HOLDIR :: SIGOBJ :: !helpdirs
97  val () = Help.specialfiles :=
98             {file = "help/Docfiles/HOL.help",
99              term = "hol", title = "HOL Overview"}
100             :: !Help.specialfiles
101end
102
103
104(*---------------------------------------------------------------------------*
105 *  Set parameters for parsing and help.                                     *
106 *---------------------------------------------------------------------------*)
107
108val _ = quotation := true
109val _ = Help.displayLines := 60;
110
111(*---------------------------------------------------------------------------*
112 *  Set up compile_theory function                                           *
113 *---------------------------------------------------------------------------*)
114
115fun compile_theory () = let
116  val name = current_theory()
117  val signame = name^"Theory.sig"
118  val smlname = name^"Theory.sml"
119  fun readable f = FileSys.access(f, [FileSys.A_READ])
120in
121  if readable signame andalso readable smlname then let
122  in
123     Meta.compileStructure ["Overlay"] signame;
124     Meta.compileStructure ["Overlay"] smlname;
125     print ("Compiled "^name^" theory files.\n")
126  end
127  else
128     print "No theory files on disk; perhaps export_theory() required.\n"
129end
130
131
132(*---------------------------------------------------------------------------*
133 * Print a banner.                                                           *
134 *---------------------------------------------------------------------------*)
135
136val build_stamp =
137 let open TextIO Path
138     val stampstr = openIn (concat(HOLDIR, concat("tools", "build-stamp")))
139     val stamp = inputAll stampstr before closeIn stampstr
140 in
141     stamp
142 end handle _ => "";
143
144val exit_string =
145    if Systeml.OS = "winNT" then
146      "To exit type <Control>-Z <Return>  (*not* quit();)"
147    else
148      "To exit type <Control>-D (*not* quit();)"
149
150
151(* ----------------------------------------------------------------------
152    if present, look at a Holmakefile in the current directory to see
153    if we should extend the loadPath
154   ---------------------------------------------------------------------- *)
155
156structure HOL_Interactive : sig
157  val toggle_quietdec : unit -> bool
158  val amquiet : unit -> bool
159  val print_banner : unit -> unit
160end =
161struct
162  fun toggle_quietdec () = (Meta.quietdec := not (!Meta.quietdec) ;
163                            !Meta.quietdec)
164  fun amquiet () = !Meta.quietdec
165  fun print_banner() =
166    TextIO.output(TextIO.stdOut,
167     "\n---------------------------------------------------------------------\n"
168     ^"       HOL-4 ["
169     ^Globals.release^" "^Lib.int_to_string(Globals.version)
170     ^" ("^Thm.kernelid^", "^build_stamp
171     ^")]\n\n"
172     ^"       For introductory HOL help, type: help \"hol\";\n"
173     ^"       "^exit_string
174     ^"\n---------------------------------------------------------------------\
175      \\n\n")
176
177end;
178
179val _ = HOL_Interactive.print_banner()
180
181local
182  open Path
183in
184  val _ = loadPath := concat (HOLDIR, concat ("tools", "Holmake")) :: !loadPath
185  val _ = load "ReadHMF.uo"
186  val _ = loadPath := tl (!loadPath)
187end;
188
189val _ = let
190  val lpsize0 = length (!loadPath)
191in
192  ReadHMF.extend_path_with_includes {verbosity = 0, lpref = loadPath};
193  if length (!loadPath) <> lpsize0 then
194    print ("** Load path (see loadPath variable) now contains " ^
195           Int.toString (length (!loadPath)) ^
196           " entries\n** after consulting Holmakefiles\n\n")
197  else ()
198end;
199
200use (Path.concat(Globals.HOLDIR, "tools/check-intconfig.sml"));
201
202(* Local variables: *)
203(* mode: sml *)
204(* end: *)
205