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