(***************************************************

    This was initially copied from /lal2/hol90_lal/mk_hol_lal.sml

 Here are the commands to run and prepare to save a hol_axi session of HOL.

1) start HOL with a clean HOL90

2) execute this file by entering

	use "mk_hol_axisem.sml";

3) save the image by entering

	save_hol_axisem "hol_axisem";

(Trent Larson says it gave weird errors when the "save..."
 is included as part of this file.)

***************************************************)

(*
 The .hol_lib file generated by new_library should be placed
 in a directory accessible to HOL (through the Globals.library_path variable).
*)

append_path "." Globals.library_path;


(* Use this to make the library file on disk: *)

(* NOTE: the list of theories cannot be empty. *)

val hol_axisem_lib = Library.new_library
    {name = "hol_axisem",
     doc = "Axiomatic semantics extensions to HOL, due to Paul E. Black.",
     path = "/users/lal/black/hol/hol_axisem/",
     parents = [       (* Required for some of the source: *)
		],
     theories = ["bits"], (* not really needed, but load_library wants
			     something loadable here *)
     code = ["partialTactics.sml"],
     help = [""],
     loaded = "fn () => (map add_theory_to_sml [];())"};

(* Load it up! *)

load_library{lib=hol_axisem_lib, theory="hol_axisem"} handle e=>Raise e;


export_theory();
close_theory();



(* Now save it under a neat name with a super special banner. *)

fun print_banner date =
   let val ver = Lib.int_to_string Globals.version_number;
       val pad_to_nine_chars = substring("          ",0,(9-(String.size ver)))
   in
 ( output(std_out, "\n\n");
   output(std_out,
"       HHH                 LL\n\
\       HHH                  LL\n\
\       HHH         OOOO      LL\n\
\       HHHHHHH    OO  OO      LL\n\
\       HHHHHHH    OO  OO      LLL               ^     ^\n\
\       HHH         OOOO      LL LL             / \\ ^ / \\\n\
\       HHH                  LL   LL           /   \\_\\   \\\n\
\       HHH                 LL     LL 90."^ver^pad_to_nine_chars^"/   \\\n\n"^
"HOL90.8 (including the LAL and axiomatic semantics extensions)\n\n"^
"Created on "^date^" using " ^ Sml_system.sml_banner ^"\n\n\n"))
	   end;

(* The following is shamelessly plagarized
     from save_hol.sml in the HOL90 source. *)
local
val init_fname = "/hol-init.sml"
val local_init_fname = "."^init_fname
in
fun save_hol_axisem str =
    let val (I,O) = Sml_system.execute ("/bin/date",[])
	val date = input_line I;
        val _ = close_in I
        val _ = close_out O
    in
       Sml_system.exportHOL str;
       print_banner date;
       if (!Globals.use_init_file)
       then if (Lib.file_exists_for_reading local_init_fname)
            then use local_init_fname
            else
		(case Sml_system.getEnv "HOME"
		     of NONE => ()
		   (*
		    We don't raise the following:
		    raise SAVE_HOL_ERR{function = "save_hol.parse_HOME",
		    message = "can not find HOME variable in environment"}
		    because non-unix systems may not have a HOME env var.
		    *)
		   | SOME home_init =>
			 let val home_init_fname = home_init ^init_fname
			 in if (Lib.file_exists_for_reading home_init_fname)
				then use home_init_fname
			    else ()
			 end)
       else ()
    end
end;

(* end of $Source: /users/lal/black/hol/Disser/RCS/mk_hol_axisem.sml,v $ *)