- removed a lot of auxiliary functions from MatitaMisc since they are now part of our extlib
-matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaLog.cmi matitaInit.cmi matitaGui.cmi \
- matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo
-matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaLog.cmx matitaInit.cmx matitaGui.cmx \
- matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx
+dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo
+dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
+ matitacleanLib.cmi
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
+ matitacleanLib.cmi
+matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \
+ matitaInit.cmi matitaDb.cmi
+matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \
+ matitaInit.cmx matitaDb.cmx
+matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \
+ matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \
+ matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
+matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \
+ matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \
+ matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
+matitac.cmo: matitacLib.cmi
+matitac.cmx: matitacLib.cmx
matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
+matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi buildTimeConf.cmo
+matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx buildTimeConf.cmx
matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \
- matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi matitaDb.cmi \
- matitaEngine.cmi
+ matitaMoo.cmi matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi \
+ matitaDb.cmi matitaEngine.cmi
matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \
- matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx matitaDb.cmx \
- matitaEngine.cmi
-matitaExcPp.cmo: matitaTypes.cmi matitaExcPp.cmi
-matitaExcPp.cmx: matitaTypes.cmx matitaExcPp.cmi
+ matitaMoo.cmx matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx \
+ matitaDb.cmx matitaEngine.cmi
+matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaExcPp.cmi
+matitaExcPp.cmx: matitaTypes.cmx matitaMoo.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi
-matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitacLib.cmi \
- matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaMathView.cmi \
+matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
+ matitaScript.cmi matitaMoo.cmi matitaMisc.cmi matitaMathView.cmi \
matitaLog.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \
matitaDisambiguator.cmi buildTimeConf.cmo matitaGui.cmi
-matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitacLib.cmx \
- matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaMathView.cmx \
+matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \
+ matitaScript.cmx matitaMoo.cmx matitaMisc.cmx matitaMathView.cmx \
matitaLog.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \
matitaDisambiguator.cmx buildTimeConf.cmx matitaGui.cmi
matitaInit.cmo: matitamakeLib.cmi matitaDb.cmi buildTimeConf.cmo \
matitaInit.cmi
matitaLog.cmo: matitaLog.cmi
matitaLog.cmx: matitaLog.cmi
+matitamakeLib.cmo: matitaLog.cmi buildTimeConf.cmo matitamakeLib.cmi
+matitamakeLib.cmx: matitaLog.cmx buildTimeConf.cmx matitamakeLib.cmi
+matitamake.cmo: matitamakeLib.cmi matitaInit.cmi
+matitamake.cmx: matitamakeLib.cmx matitaInit.cmx
matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
buildTimeConf.cmo matitaMathView.cmi
buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \
buildTimeConf.cmx matitaMisc.cmi
+matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \
+ matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \
+ buildTimeConf.cmo
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.cmx \
+ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \
+ buildTimeConf.cmx
+matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi
+matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi
matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \
matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi
matitaSync.cmi
matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi
matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi
-matitac.cmo: matitacLib.cmi
-matitac.cmx: matitacLib.cmx
-matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
- matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
-matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
- matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
-matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- buildTimeConf.cmo
-matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- buildTimeConf.cmx
-matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- matitacleanLib.cmi
-matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- matitacleanLib.cmi
-matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \
- buildTimeConf.cmo
-matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \
- buildTimeConf.cmx
-matitamake.cmo: matitamakeLib.cmi matitaInit.cmi
-matitamake.cmx: matitamakeLib.cmx matitaInit.cmx
-matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \
- matitamakeLib.cmi
-matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \
- matitamakeLib.cmi
matitaDisambiguator.cmi: matitaTypes.cmi
matitaEngine.cmi: matitaTypes.cmi
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmi: matitaTypes.cmi
+matitaMoo.cmi: matitaTypes.cmi
matitaScript.cmi: matitaTypes.cmi
matitaSync.cmi: matitaTypes.cmi
buildTimeConf.cmo \
matitaLog.cmo \
matitaTypes.cmo \
+ matitaMoo.cmo \
matitaExcPp.cmo \
matitaMisc.cmo \
matitaDb.cmo \
buildTimeConf.cmo \
matitaLog.cmo \
matitaTypes.cmo \
+ matitaMoo.cmo \
matitaExcPp.cmo \
matitaMisc.cmo \
matitaDb.cmo \
$(NULL)
CLEANCMOS = $(CCMOS)
MAKECMOS = $(CCMOS)
+PROGRAMS = matita matitac matitatop cicbrowser matitadep matitaclean matitamake
+PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS))
-all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake
+all: matita.conf.xml $(PROGRAMS) dump_moo
matita.conf.xml: matita.conf.xml.sample
@if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
CLEANLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CLEANREQUIRES))
MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MAKEREQUIRES))
MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES))
-opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt matitaclean.opt matitamake.opt
+opt: $(PROGRAMS_OPT)
else
opt:
@echo "Native code compilation is disabled"
matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
+dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml
+ $(OCAMLC) $(PKGS) -linkpkg -o $@ $^
+
matitac: $(CLIB_DEPS) $(CCMOS) matitac.ml
$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml
matitac.opt: $(CLIBX_DEPS) $(CCMXS) matitac.ml
matitadep matitadep.opt \
matitaclean matitaclean.opt \
matitamake matitamake.opt \
- matitatop matitatop.opt
+ matitatop matitatop.opt \
+ dump_moo
distclean: clean
rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
rm -f config.log config.status Makefile buildTimeConf.ml
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+let arg_spec =
+ let std_arg_spec = [] in
+ let debug_arg_spec = [] in
+ std_arg_spec @ debug_arg_spec
+
+let usage =
+ sprintf "MatitaC v%s\nUsage: dump_moo [option ...] file.moo\nOptions:"
+ BuildTimeConf.version
+
+let _ =
+ let moos = ref [] in
+ let add_moo fname = moos := fname :: !moos in
+ Arg.parse arg_spec add_moo usage;
+ if !moos = [] then begin print_endline usage; exit 1 end;
+ List.iter
+ (fun fname ->
+ if not (Sys.file_exists fname) then
+ MatitaLog.error (sprintf "Can't find moo '%s', skipping it." fname)
+ else begin
+ printf "%s:\n" fname; flush stdout;
+ let commands = MatitaMoo.load_moo ~fname in
+ List.iter
+ (fun cmd ->
+ printf " %s\n" (GrafiteAstPp.pp_command cmd); flush stdout)
+ commands
+ end)
+ (List.rev !moos)
+
open MatitaGtkMisc
open MatitaTypes
-open MatitaMisc
(** {2 Initialization} *)
) status projections
(* to avoid a long list of recursive functions *)
-let eval_from_dump_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
let disambiguate_obj status obj =
let uri =
let status = ref status in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
- !eval_from_dump_ref status moopath (fun _ _ -> ());
+ !eval_from_moo_ref status moopath (fun _ _ -> ());
!status
| GrafiteAst.Set (loc, name, value) ->
let value =
| GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c
-let eval_from_dump ?do_heavy_checks ?include_paths ?clean_baseuri status fname
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
cb
=
- let ic = open_in fname in
- let moo = Marshal.from_channel ic in
- close_in ic;
+ let moo = MatitaMoo.load_moo fname in
List.iter
(fun ast ->
let ast =
GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
GrafiteAst.Command (DisambiguateTypes.dummy_floc,
- (GrafiteAst.reash_uris ast)))
+ (GrafiteAst.reash_cmd_uris ast)))
in
cb !status ast;
status :=
with End_of_file -> ()
(* to avoid a long list of recursive functions *)
-let _ = eval_from_dump_ref := eval_from_dump
+let _ = eval_from_moo_ref := eval_from_moo
let eval_from_stream_greedy
?do_heavy_checks ?include_paths ?clean_baseuri status str cb
| Unix.Unix_error (code, api, param) ->
let err = Unix.error_message code in
"Unix Error (" ^ api ^ "): " ^ err
+ | MatitaMoo.Corrupt_moo fname ->
+ sprintf ".moo file '%s' is corrupt (shorter than expected)" fname
+ | MatitaMoo.Checksum_failure fname ->
+ sprintf "checksum failed for .moo file '%s', please recompile it'" fname
+ | MatitaMoo.Version_mismatch fname ->
+ sprintf
+ (".moo file '%s' has been compiled by a different version of matita, "
+ ^^ "please recompile it")
+ fname
| exn -> "Uncaught exception: " ^ Printexc.to_string exn
let ask_and_save_moo_if_needed parent fname status =
let save () =
- MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+ let moo_fname = MatitaMisc.obj_file_of_script fname in
+ MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
if (MatitaScript.instance ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.No_proof
then
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
begin
- if is_regular fname && not(_only_directory) then
+ if HExtlib.is_regular fname && not (_only_directory) then
return (Some fname)
- else if _only_directory && is_dir fname then
+ else if _only_directory && HExtlib.is_dir fname then
return (Some fname)
end
else
match href_callback with
| None -> ()
| Some f ->
- (match MatitaMisc.split href_value with
+ (match HExtlib.split href_value with
| [ uri ] -> f uri
| uris ->
let menu = GMenu.menu () in
self#_showMath;
match self#script#status.proof_status with
| Proof (uri, metasenv, bo, ty) ->
- let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| Incomplete_proof ((uri, metasenv, bo, ty), _) ->
- let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| _ -> self#blank ()
(** this is what the browser does when you enter a string an hit enter *)
method loadInput txt =
- let txt = MatitaMisc.trim_blanks txt in
+ let txt = HExtlib.trim_blanks txt in
let fix_uri txt =
UriManager.string_of_uri
(UriManager.strip_xpointer (UriManager.uri_of_string txt))
let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
-let is_dir fname =
- try
- (Unix.stat fname).Unix.st_kind = Unix.S_DIR
- with Unix.Unix_error _ -> false
-
-let is_regular fname =
- try
- (Unix.stat fname).Unix.st_kind = Unix.S_REG
- with Unix.Unix_error _ -> false
-
-let input_file fname =
- let size = (Unix.stat fname).Unix.st_size in
- let buf = Buffer.create size in
- let ic = open_in fname in
- Buffer.add_channel buf ic size;
- close_in ic;
- Buffer.contents buf
-
-let output_file data file =
- let oc = open_out file in
- output_string oc data;
- close_out oc
-
let absolute_path file =
if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
else
s
-let mkdir path =
- let components = Str.split (Str.regexp "/") path in
- let rec aux where = function
- | [] -> ()
- | piece::tl ->
- let path = where ^ "/" ^ piece in
- (try
- Unix.mkdir path 0o755
- with
- | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
- | Unix.Unix_error (e,_,_) ->
- raise
- (Failure
- ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
- aux path tl
- in
- aux "" components
-
-let trim_blanks =
- let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in
- fun s -> (Pcre.extract ~rex s).(1)
-
-let split ?(char = ' ') s =
- let pieces = ref [] in
- let rec aux idx =
- match (try Some (String.index_from s idx char) with Not_found -> None) with
- | Some pos ->
- pieces := String.sub s idx (pos - idx) :: !pieces;
- aux (pos + 1)
- | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces
- in
- aux 0;
- List.rev !pieces
-
let empty_mathml () =
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
~qualifiedName:(Gdome.domString "math") ~doctype:None
let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
-let unopt = function None -> failwith "unopt: None" | Some v -> v
-
let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
let end_ma_RE = Pcre.regexp "\\.ma$"
in
aux l
-let debug_wrap name f =
- prerr_endline (sprintf "debug_wrap: ==>> %s" name);
- let res = f () in
- prerr_endline (sprintf "debug_wrap: <<== %s" name);
- res
-
(** removes a file if it exists *)
val safe_remove: string -> unit
-val is_dir: string -> bool (** @return true if file is a directory *)
-val is_regular: string -> bool (** @return true if file is a regular file *)
-
-val input_file: string -> string (** read all the contents of file to string *)
-val output_file: string -> string -> unit (** write string to file *)
-
val absolute_path: string -> string
(** @return true if file is a (textual) proof script *)
* it *)
val append_phrase_sep: string -> string
-val trim_blanks: string -> string
val strip_trailing_slash: string -> string
val normalize_dir: string -> string (** add trailing "/" if missing *)
val strip_suffix: suffix:string -> string -> string
- (* split a string at character, char defaults to ' ' *)
-val split: ?char:char -> string -> string list
-
val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
(** @return tl tail of a list starting at a given element
* @raise Not_found *)
val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
- (** @raise Failure *)
-val unopt: 'a option -> 'a
-
(** Gdome.element of a MathML document whose rendering should be blank. Used
* by cicBrowser to render "about:blank" document *)
val empty_mathml: unit -> Gdome.document
* first time it gets called. Next invocation will return first value *)
val singleton: (unit -> 'a) -> (unit -> 'a)
- (** create a directory, building also parents if needed
- * @raise Failure when unable to create some directory *)
-val mkdir: string -> unit
-
val qualify: MatitaTypes.status -> string -> string
val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status
val obj_file_of_baseuri: string -> string
val obj_file_of_script: string -> string
- (** invoke a given function and return its value; in addition il will print
- * the given string before invoking it and "/" ^ the given string afterwards.
- * This permit tracing of functions which does not return a value *)
-val debug_wrap: string -> (unit -> 'a) -> 'a
-
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception Checksum_failure of string
+exception Corrupt_moo of string
+exception Version_mismatch of string
+
+let marshal_flags = []
+
+(** .moo file format
+ * - an integer -- magic number -- denoting the version of the dumped data
+ * structure. Different magic numbers stand for incompatible data structures
+ * - an integer -- checksum -- denoting the hash value (computed with
+ * Hashtbl.hash) of the string representation of the dumped data structur
+ * - marshalled list of GrafiteAst.command
+ *)
+
+let save_moo ~fname moo =
+ let oc = open_out fname in
+ let marshalled_moo = Marshal.to_string (List.rev moo) marshal_flags in
+ let checksum = Hashtbl.hash marshalled_moo in
+ output_binary_int oc GrafiteAst.magic;
+ output_binary_int oc checksum;
+ output_string oc marshalled_moo;
+ close_out oc
+
+let load_moo ~fname =
+ let ic = open_in fname in
+ HExtlib.finally
+ (fun () -> close_in ic)
+ (fun () ->
+ try
+ let moo_magic = input_binary_int ic in
+ if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname);
+ let moo_checksum = input_binary_int ic in
+ let marshalled_moo = HExtlib.input_all ic in
+ let checksum = Hashtbl.hash marshalled_moo in
+ if checksum <> moo_checksum then raise (Checksum_failure fname);
+ let (moo: MatitaTypes.ast_command list) =
+ Marshal.from_string marshalled_moo 0
+ in
+ moo
+ with End_of_file -> raise (Corrupt_moo fname))
+ ()
+
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** name of the corrupt .moo file *)
+exception Checksum_failure of string
+exception Corrupt_moo of string
+exception Version_mismatch of string
+
+val save_moo: fname:string -> MatitaTypes.ast_command list -> unit
+
+ (** @raise Corrupt_moo *)
+val load_moo: fname:string -> MatitaTypes.ast_command list
+
let l = MQ.match_term ~dbd term in
let query_url =
MatitaMisc.strip_suffix ~suffix:"."
- (MatitaMisc.trim_blanks unparsed_text)
+ (HExtlib.trim_blanks unparsed_text)
in
let entry = `Whelp (query_url, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
List.iter (fun o -> o status) observers
method loadFromFile f =
- buffer#set_text (MatitaMisc.input_file f);
+ buffer#set_text (HExtlib.input_file f);
self#reset_buffer;
buffer#set_modified false
buffer#set_modified false
method template () =
- let template = MatitaMisc.input_file BuildTimeConf.script_template in
+ let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
guistuff.filenamedata <-
(None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
let save_object_to_disk status uri obj ugraph univlist =
let ensure_path_exists path =
let dir = Filename.dirname path in
- MatitaMisc.mkdir dir
+ HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
paths_and_uris_of_obj uri status
in
let path_scheme_of path = "file://" ^ path in
- List.iter MatitaMisc.mkdir
- (List.map Filename.dirname [innertypespath; xmlpath]);
+ List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
(* now write to disk *)
ensure_path_exists xmlpath;
Xml.pp ~gzip:true xml (Some xmlpath);
CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
(* we return a list of uri,path we registered/created *)
- (uri,xmlpath) :: (innertypesuri,innertypespath) ::
+ (uri,xmlpath) ::
(univgraphuri,xmlunivgraphpath) ::
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
Sys.catch_break true;
interactive_loop ()
-let dump_moo_to_file file moo =
- let os = open_out (MatitaMisc.obj_file_of_script file) in
- Marshal.to_channel os (List.rev moo) [];
- close_out os
-
let main ~mode =
MatitaInit.initialize_all ();
status := Some (ref (Lazy.force MatitaEngine.initial_status));
end
else
begin
- dump_moo_to_file fname moo_content_rev;
+ let moo_fname = MatitaMisc.obj_file_of_script fname in
+ MatitaMoo.save_moo moo_fname moo_content_rev;
MatitaLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
exit 0
val go : unit -> unit
val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
-(** fname is the .ma *)
-val dump_moo_to_file:
- string ->
- (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list ->
- unit
-
(** clean_exit n
if n = Some n it performs an exit [n] after a complete clean-up of what was
partially compiled
let initialize () =
(* create a base env if none *)
- MatitaMisc.mkdir (pool ());
+ HExtlib.mkdir (pool ());
(* load developments *)
match ls_dir (pool ()) with
| None -> logger `Error ("Unable to list directory " ^ pool ())
(fun name ->
let root =
try
- Some (MatitaMisc.input_file (pool () ^ name ^ rootfile))
+ Some (HExtlib.input_file (pool () ^ name ^ rootfile))
with Unix.Unix_error _ ->
logger `Warning ("Malformed development " ^ name);
None
(* dumps the deveopment to disk *)
let dump_development devel =
let devel_dir = pool () ^ devel.name in
- MatitaMisc.mkdir devel_dir;
- MatitaMisc.output_file devel.root (devel_dir ^ rootfile);
+ HExtlib.mkdir devel_dir;
+ HExtlib.output_file ~filename:(devel_dir ^ rootfile) ~text:devel.root
;;
let list_known_developments () =
let rebuild_makefile development =
let makefilepath = makefile_for_development development in
let template =
- MatitaMisc.input_file BuildTimeConf.matitamake_makefile_template
+ HExtlib.input_file BuildTimeConf.matitamake_makefile_template
in
let cc = BuildTimeConf.runtime_base_dir ^ "/matitac" ^ am_i_opt () in
let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in
let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in
let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in
let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
- MatitaMisc.output_file template makefilepath
+ HExtlib.output_file ~filename:makefilepath ~text:template
(* creates a new development if possible *)
let initialize_development name dir =
projects / helm.git / commitdiff