From: Claudio Sacerdoti Coen Date: Fri, 8 Sep 2006 10:16:52 +0000 (+0000) Subject: Dead code (that produces an ugly rendering) removed. X-Git-Tag: make_still_working~6922 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5c1f34cd226898525168e470d3e2ec273699826;p=helm.git Dead code (that produces an ugly rendering) removed. --- diff --git a/helm/software/components/acic_content/contentPp.ml b/helm/software/components/acic_content/contentPp.ml deleted file mode 100644 index ca89fad7d..000000000 --- a/helm/software/components/acic_content/contentPp.ml +++ /dev/null @@ -1,158 +0,0 @@ -(* Copyright (C) 2000, 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 *) -(* *) -(* Andrea Asperti *) -(* 17/06/2003 *) -(* *) -(***************************************************************************) - -(* $Id$ *) - -exception ContentPpInternalError;; -exception NotEnoughElements;; -exception TO_DO - -(* Utility functions *) - - -let string_of_name = - function - Some s -> s - | None -> "_" -;; - -(* get_nth l n returns the nth element of the list l if it exists or *) -(* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = - match (n,l) with - (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements -;; - -let rec blanks n = - if n = 0 then "" - else (" " ^ (blanks (n-1)));; - -let rec pproof (p: Cic.annterm Content.proof) indent = - let module Con = Content in - let new_indent = - (match p.Con.proof_name with - Some s -> - prerr_endline - ((blanks indent) ^ "(" ^ s ^ ")"); flush stderr ;(indent + 1) - | None ->indent) in - let new_indent1 = - if (p.Con.proof_context = []) then new_indent - else - (pcontext p.Con.proof_context new_indent; (new_indent + 1)) in - papply_context p.Con.proof_apply_context new_indent1; - pconclude p.Con.proof_conclude new_indent1; - -and pcontext c indent = - List.iter (pcontext_element indent) c - -and pcontext_element indent = - let module Con = Content in - function - `Declaration d -> - (match d.Con.dec_name with - Some s -> - prerr_endline - ((blanks indent) - ^ "Assume " ^ s ^ " : " - ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.dec_type))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> - prerr_endline - ((blanks indent) - ^ "Suppose " ^ s ^ " : " - ^ (CicPp.ppterm (Deannotate.deannotate_term h.Con.dec_type))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Proof p -> pproof p indent - | `Definition d -> - (match d.Con.def_name with - Some s -> - prerr_endline - ((blanks indent) ^ "Let " ^ s ^ " = " - ^ (CicPp.ppterm (Deannotate.deannotate_term d.Con.def_term))); - flush stderr - | None -> - prerr_endline ((blanks indent) ^ "NO NAME!!")) - | `Joint ho -> - prerr_endline ((blanks indent) ^ "Joint Def"); - flush stderr - -and papply_context ac indent = - List.iter(function p -> (pproof p indent)) ac - -and pconclude concl indent = - let module Con = Content in - prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr; - pargs concl.Con.conclude_args indent; - match concl.Con.conclude_conclusion with - None -> prerr_endline ((blanks indent) ^"No conclude conclusion");flush stderr - | Some t -> prerr_endline ((blanks indent) ^ "conclude" ^ concl.Con.conclude_method ^ (CicPp.ppterm (Deannotate.deannotate_term t)));flush stderr - -and pargs args indent = - List.iter (parg indent) args - -and parg indent = - let module Con = Content in - function - Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ n) - | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise") - | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma") - | Con.Term t -> - prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t))) - | Con.ArgProof p -> pproof p (indent+1) - | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!") -;; - -let print_proof p = pproof p 0;; - -let print_obj (_,_,_,obj) = - match obj with - `Decl (_,decl) -> - pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element) - | `Def (_,_,def) -> - pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element) - | `Joint _ as jo -> pcontext_element 0 jo -;; - - - - - diff --git a/helm/software/components/acic_content/contentPp.mli b/helm/software/components/acic_content/contentPp.mli deleted file mode 100644 index a160ab1ff..000000000 --- a/helm/software/components/acic_content/contentPp.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* Copyright (C) 2000, 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/. - *) - -val print_proof: Cic.annterm Content.proof -> unit - -val print_obj: Cic.annterm Content.cobj -> unit - -val parg: int -> Cic.annterm Content.arg ->unit