From 541a200b13431987114dd3fd88ec9764cee1e772 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Feb 2005 16:45:22 +0000 Subject: [PATCH] better owner hadling better basedir non existent path handling matitaDb module to set up and clean owner metadata environment --- helm/matita/.depend | 66 +++++++------- helm/matita/Makefile.in | 4 +- helm/matita/matita.ml | 11 ++- helm/matita/matitaDb.ml | 134 +++++++++++++++++++++++++++++ helm/matita/matitaDb.mli | 28 ++++++ helm/matita/matitaDisambiguator.ml | 2 +- helm/matita/matitaInterpreter.ml | 18 ++++ helm/matita/matitac.ml | 7 +- 8 files changed, 233 insertions(+), 37 deletions(-) create mode 100644 helm/matita/matitaDb.ml create mode 100644 helm/matita/matitaDb.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 53ee0197f..18f464afd 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,52 +1,54 @@ +matita.cmo: buildTimeConf.cmo matitaDb.cmi matitaDisambiguator.cmi \ + matitaGtkMisc.cmi matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi \ + matitaMisc.cmi matitaProof.cmi matitaTypes.cmi +matita.cmx: buildTimeConf.cmx matitaDb.cmx matitaDisambiguator.cmx \ + matitaGtkMisc.cmx matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx \ + matitaMisc.cmx matitaProof.cmx matitaTypes.cmx matitaCicMisc.cmo: matitaTypes.cmi matitaCicMisc.cmi matitaCicMisc.cmx: matitaTypes.cmx matitaCicMisc.cmi -matitac.cmo: matitaTypes.cmi matitaInterpreter.cmi matitaDisambiguator.cmi \ - buildTimeConf.cmo -matitac.cmx: matitaTypes.cmx matitaInterpreter.cmx matitaDisambiguator.cmx \ - buildTimeConf.cmx -matitaConsole.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmo matitaConsole.cmi -matitaConsole.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ - buildTimeConf.cmx matitaConsole.cmi +matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaMisc.cmi \ + matitaTypes.cmi matitaConsole.cmi +matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaMisc.cmx \ + matitaTypes.cmx matitaConsole.cmi +matitaDb.cmo: matitaDb.cmi +matitaDb.cmx: matitaDb.cmi matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.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: matitaMisc.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi \ - matitaConsole.cmi buildTimeConf.cmo matitaGui.cmi -matitaGui.cmx: matitaMisc.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ - matitaConsole.cmx buildTimeConf.cmx matitaGui.cmi -matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi \ - matitaCicMisc.cmi matitaInterpreter.cmi -matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx \ - matitaCicMisc.cmx matitaInterpreter.cmi -matitaMathView.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi \ - matitaGui.cmi matitaGtkMisc.cmi matitaCicMisc.cmi buildTimeConf.cmo \ +matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi +matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ + matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi +matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ + matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi +matitaInterpreter.cmo: matitaCicMisc.cmi matitaMisc.cmi matitaProof.cmi \ + matitaTypes.cmi matitaInterpreter.cmi +matitaInterpreter.cmx: matitaCicMisc.cmx matitaMisc.cmx matitaProof.cmx \ + matitaTypes.cmx matitaInterpreter.cmi +matitaMathView.cmo: buildTimeConf.cmo matitaCicMisc.cmi matitaGtkMisc.cmi \ + matitaGui.cmi matitaMisc.cmi matitaProof.cmi matitaTypes.cmi \ matitaMathView.cmi -matitaMathView.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx \ - matitaGui.cmx matitaGtkMisc.cmx matitaCicMisc.cmx buildTimeConf.cmx \ +matitaMathView.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaGtkMisc.cmx \ + matitaGui.cmx matitaMisc.cmx matitaProof.cmx matitaTypes.cmx \ matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ - matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaDisambiguator.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \ - matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaDisambiguator.cmx buildTimeConf.cmx -matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmi buildTimeConf.cmo \ +matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmi matitaTypes.cmi \ matitaProof.cmi -matitaProof.cmx: matitaTypes.cmx matitaCicMisc.cmx buildTimeConf.cmx \ +matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi +matitac.cmo: buildTimeConf.cmo matitaDb.cmi matitaDisambiguator.cmi \ + matitaInterpreter.cmi matitaTypes.cmi +matitac.cmx: buildTimeConf.cmx matitaDb.cmx matitaDisambiguator.cmx \ + matitaInterpreter.cmx matitaTypes.cmx matitaCicMisc.cmi: matitaTypes.cmi matitaConsole.cmi: matitaTypes.cmi matitaDisambiguator.cmi: matitaTypes.cmi -matitaGtkMisc.cmi: matitaTypes.cmi matitaGeneratedGui.cmi -matitaGui.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaConsole.cmi +matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmi +matitaGui.cmi: matitaConsole.cmi matitaGeneratedGui.cmi matitaTypes.cmi matitaInterpreter.cmi: matitaTypes.cmi matitaMathView.cmi: matitaTypes.cmi matitaProof.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 07fd7f338..aadfd26ad 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -66,9 +66,9 @@ matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml cicbrowser: matita - test -f $@ || ln $< $@ + test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt - test -f $@ || ln $< $@ + test -f $@ || ln -s $< $@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) $< > matitaGeneratedGui.ml diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 40f2077cf..bc42bba54 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -43,7 +43,12 @@ let dbd = ~user:(Helm_registry.get "db.user") ~database:(Helm_registry.get "db.database") () -let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner") + +let owner = (Helm_registry.get "matita.owner") ;; +let _ = MetadataTypes.ownerize_tables owner ;; +let _ = MatitaDb.clean_owner_environment dbd owner ;; +let _ = MatitaDb.create_owner_environment dbd owner ;; + let gui = MatitaGui.instance () let disambiguator = new MatitaDisambiguator.disambiguator ~parserr ~dbd @@ -51,7 +56,11 @@ let disambiguator = ~chooseInterp:(interactive_interp_choice ~gui) () +let currentProof = new MatitaProof.currentProof + let currentProof = MatitaProof.instance () + + let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = let set_goal goal = diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml new file mode 100644 index 000000000..a6eb73ded --- /dev/null +++ b/helm/matita/matitaDb.ml @@ -0,0 +1,134 @@ +(* Copyright (C) 2004, 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 clean_owner_environment dbd owner = + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let conclno_tbl = MetadataTypes.conclno_tbl () in + let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in + let statements = [ + sprintf "DROP TABLE %s ;" obj_tbl; + sprintf "DROP TABLE %s ;" sort_tbl; + sprintf "DROP TABLE %s ;" rel_tbl; + sprintf "DROP TABLE %s ;" name_tbl; + sprintf "DROP TABLE %s ;" conclno_tbl; + sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in +(* +DROP INDEX refObj_source ON refObj (source); +DROP INDEX refObj_target ON refObj (h_occurrence); +DROP INDEX refObj_position ON refObj (h_position); +DROP INDEX refSort_source ON refSort (source); +DROP INDEX objectName_value ON objectName (value); +DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source); +DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no); +DROP INDEX no_concl_hyp_source ON no_concl_hyp (source); +DROP INDEX no_concl_hyp_no ON no_concl_hyp (no); +*) + (try + MetadataDb.clean ~dbd + with + exn -> + match Mysql.errno dbd with + | Mysql.No_such_table -> () + | _ -> raise exn + | _ -> () + ); + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with + exn -> + match Mysql.errno dbd with + | Mysql.No_such_table -> () + | _ -> raise exn + | _ -> () + ) statements +;; + +let create_owner_environment dbd owner = + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let conclno_tbl = MetadataTypes.conclno_tbl () in + let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in + let statements = [ + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_occurrence varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer + );" obj_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null, + h_sort varchar(255) binary not null + );" sort_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null + );" rel_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + value varchar(255) binary not null + );" name_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + no tinyint(4) not null + );" conclno_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + no tinyint(4) not null + );" conclno_hyp_tbl ] in +(* +CREATE INDEX refObj_source ON refObj (source); +CREATE INDEX refObj_target ON refObj (h_occurrence); +CREATE INDEX refObj_position ON refObj (h_position); +CREATE INDEX refSort_source ON refSort (source); +CREATE INDEX objectName_value ON objectName (value); +CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source); +CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no); +CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source); +CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no); +*) + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with + exn -> + let status = Mysql.status dbd in + match status with + | Mysql.StatusError Mysql.Table_exists_error -> () + | Mysql.StatusError _ -> raise exn + | _ -> () + ) statements +;; + diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli new file mode 100644 index 000000000..b470ec596 --- /dev/null +++ b/helm/matita/matitaDb.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2004, 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/ + *) + +val clean_owner_environment : Mysql.dbd -> string -> unit +val create_owner_environment : Mysql.dbd -> string -> unit + diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 5b95f4192..15f21e509 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -55,7 +55,7 @@ class disambiguator end in let module Disambiguator = Disambiguate.Make (Callbacks) in - Disambiguator.disambiguate_term + Disambiguator.disambiguate_term in object (self) val mutable parserr: parserr = parserr diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 640b7406e..88e44ea7a 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -256,6 +256,21 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = let save_object_to_disk uri obj = + let ensure_path_exists path = + let dir = Filename.dirname path in + try + let stats = Unix.stat dir in + if stats.Unix.st_kind <> Unix.S_DIR then + raise (Failure (dir ^ " already exists and is not a directory")) + else + () + with + Unix.Unix_error (_,_,_) -> + let pstatus = Unix.system ("mkdir -p " ^ dir) in + match pstatus with + | Unix.WEXITED n when n = 0 -> () + | _ -> raise (Failure ("Unable to create " ^ dir)) + in (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object ~eta_fix:false obj @@ -286,7 +301,9 @@ let let path_scheme_of path = "file:/" ^ path in (* now write to disk *) + ensure_path_exists innertypespath; Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ; + ensure_path_exists xmlpath; Xml.pp ~quiet:true xml (Some xmlpath) ; (* now register to the getter *) @@ -297,6 +314,7 @@ let (match bodyxml,bodyuri with None,None -> () | Some bodyxml,Some bodyuri-> + ensure_path_exists xmlbodypath; Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ; Http_getter.register' bodyuri (path_scheme_of xmlbodypath) | _-> assert false) diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index 87c30cfea..c29b50779 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -72,7 +72,12 @@ let dbd = ~user:(Helm_registry.get "db.user") ~database:(Helm_registry.get "db.database") () -let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner") + +let owner = (Helm_registry.get "matita.owner") ;; +let _ = MetadataTypes.ownerize_tables owner ;; +let _ = MatitaDb.clean_owner_environment dbd owner ;; +let _ = MatitaDb.create_owner_environment dbd owner ;; + let disambiguator = new MatitaDisambiguator.disambiguator ~parserr ~dbd ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback -- 2.39.2