From: Enrico Tassi Date: Tue, 28 Jun 2005 15:48:01 +0000 (+0000) Subject: misc -> domMisc X-Git-Tag: INDEXING_NO_PROOFS~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc9cc53fbb0cb8676106e0c4d74053bbe1ac1a8e;p=helm.git misc -> domMisc --- diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index b05f4e1ad..4203ff228 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -35,16 +35,16 @@ sequent2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \ sequent2pres.cmi sequent2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \ sequent2pres.cmi -misc.cmo: misc.cmi -misc.cmx: misc.cmi +domMisc.cmo: domMisc.cmi +domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi sequentPp.cmo: cic2Xml.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx sequentPp.cmi applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \ - misc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi + content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \ - misc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi + content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 3c43c338d..4675291d4 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -14,7 +14,7 @@ INTERFACE_FILES = \ acic2Ast.mli \ cicAstPp.mli ast2pres.mli content2pres.mli \ sequent2pres.mli \ - misc.mli xml2Gdome.mli sequentPp.mli \ + domMisc.mli xml2Gdome.mli sequentPp.mli \ applyTransformation.mli \ tacticAstPp.mli boxPp.mli tacticAst2Box.mli IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 57d26f168..560f6a0d1 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -45,7 +45,7 @@ let mml_of_cic_sequent metasenv sequent = let pres_sequent = (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in let xmlpres = mpres_document pres_sequent in - Xml2Gdome.document_of_xml Misc.domImpl xmlpres, + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, (asequent, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) @@ -60,7 +60,7 @@ let mml_of_cic_object obj = in let pres = Content2pres.content2pres ~ids_to_inner_sorts content in let xmlpres = mpres_document pres in - let mathml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in + let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in (mathml,(annobj, (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) diff --git a/helm/ocaml/cic_transformations/domMisc.ml b/helm/ocaml/cic_transformations/domMisc.ml new file mode 100644 index 000000000..56d542556 --- /dev/null +++ b/helm/ocaml/cic_transformations/domMisc.ml @@ -0,0 +1,49 @@ +(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(******************************************************************************) + +let domImpl = Gdome.domImplementation () +let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" +let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" +let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML" +let boxml_ns = Gdome.domString "http://helm.cs.unibo.it/2003/BoxML" + + (* TODO BRRRRR .... *) + (** strip first 4 line of a string, used to strip xml declaration and doctype + declaration from XML strings generated by Xml.pp_to_string *) +let strip_xml_headings = + let xml_headings_RE = Pcre.regexp "^.*\n.*\n.*\n.*\n" in + fun s -> + Pcre.replace ~rex:xml_headings_RE s + diff --git a/helm/ocaml/cic_transformations/domMisc.mli b/helm/ocaml/cic_transformations/domMisc.mli new file mode 100644 index 000000000..d0779d1e7 --- /dev/null +++ b/helm/ocaml/cic_transformations/domMisc.mli @@ -0,0 +1,46 @@ +(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 15/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +(* TODO rename this module into at least something like CicMisc *) + +val domImpl : Gdome.domImplementation + +val helm_ns : Gdome.domString (** HELM namespace *) +val xlink_ns : Gdome.domString (** XLink namespace *) +val mathml_ns : Gdome.domString (** MathML namespace *) +val boxml_ns : Gdome.domString (** BoxML namespace *) + +val strip_xml_headings: string -> string + diff --git a/helm/ocaml/cic_transformations/misc.ml b/helm/ocaml/cic_transformations/misc.ml deleted file mode 100644 index 56d542556..000000000 --- a/helm/ocaml/cic_transformations/misc.ml +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) - -let domImpl = Gdome.domImplementation () -let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" -let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" -let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML" -let boxml_ns = Gdome.domString "http://helm.cs.unibo.it/2003/BoxML" - - (* TODO BRRRRR .... *) - (** strip first 4 line of a string, used to strip xml declaration and doctype - declaration from XML strings generated by Xml.pp_to_string *) -let strip_xml_headings = - let xml_headings_RE = Pcre.regexp "^.*\n.*\n.*\n.*\n" in - fun s -> - Pcre.replace ~rex:xml_headings_RE s - diff --git a/helm/ocaml/cic_transformations/misc.mli b/helm/ocaml/cic_transformations/misc.mli deleted file mode 100644 index d0779d1e7..000000000 --- a/helm/ocaml/cic_transformations/misc.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -(* TODO rename this module into at least something like CicMisc *) - -val domImpl : Gdome.domImplementation - -val helm_ns : Gdome.domString (** HELM namespace *) -val xlink_ns : Gdome.domString (** XLink namespace *) -val mathml_ns : Gdome.domString (** MathML namespace *) -val boxml_ns : Gdome.domString (** BoxML namespace *) - -val strip_xml_headings: string -> string - diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 1525cfd8b..191323599 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -128,6 +128,7 @@ type obj = type ('term,'obj) command = | Set of loc * string * string + | Drop of loc | Qed of loc (** name. * Name is needed when theorem was started without providing a name diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index bc4346e91..ee099e420 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -220,6 +220,7 @@ let pp_obj = function let pp_command = function | Qed _ -> "qed" + | Drop _ -> "drop" | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" | Alias (_,s) -> pp_alias s