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
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 = \
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))
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)))
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
-
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
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
projects / helm.git / commitdiff