X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fannotation2Xml.ml;fp=helm%2Finterface%2Fannotation2Xml.ml;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=b75f2bc29d55313dbfb6564d5bae823fb7ba4065;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git

diff --git a/helm/interface/annotation2Xml.ml b/helm/interface/annotation2Xml.ml
deleted file mode 100644
index b75f2bc29..000000000
--- a/helm/interface/annotation2Xml.ml
+++ /dev/null
@@ -1,228 +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/.
- *)
-
-(*CSC codice cut & paste da cicPp e xmlcommand *)
-
-exception ImpossiblePossible;;
-exception NotImplemented;;
-exception BinderNotSpecified;;
-
-let dtdname = "http://localhost:8081/getdtd?url=annotations.dtd";;
-
-(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term =
- let rec aux =
-  let module C = Cic in
-  let module X = Xml in
-  let module U = UriManager in
-    function
-       C.ARel (id,ann,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AVar (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMeta (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.ASort (id,ann,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AImplicit _ -> raise NotImplemented
-     | C.AProd (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.ACast (id,ann,v,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux v ;
-           aux t
-        >]
-     | C.ALambda (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.ALetIn (id,ann,_,s,t) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux s ;
-           aux t
-        >]
-     | C.AAppl (id,ann,li) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
-        >]
-     | C.AConst (id,ann,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AAbst (id,ann,_) -> raise NotImplemented
-     | C.AMutInd (id,ann,_,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMutConstruct (id,ann,_,_,_,_) ->
-        (match !ann with
-            None -> [<>]
-          | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-        )
-     | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           aux ty ;
-           aux te ;
-           List.fold_right
-            (fun x i -> [< aux x ; i>])
-            patterns [<>]
-        >]
-     | C.AFix (id, ann, _, funs) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           List.fold_right
-            (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
-        >]
-     | C.ACoFix (id, ann,no,funs) ->
-        [< (match !ann with
-               None -> [<>]
-             | Some ann ->
-                (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
-           ) ;
-           List.fold_right
-            (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
-        >]
- in
-  aux
-;;
-
-let print_mutual_inductive_type (_,_,arity,constructors) =
- [< print_term arity ;
-    List.fold_right
-     (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
- >]
-;;
-
-let target_uri_of_annotation_uri uri =
- Str.replace_first (Str.regexp "\.ann$") "" (UriManager.string_of_uri uri)
-;;
-
-let pp_annotation obj curi =
- let module C = Cic in
- let module X = Xml in
-  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-     X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
-     X.xml_nempty "Annotations" ["of", target_uri_of_annotation_uri curi]
-      begin
-       match obj with
-         C.ADefinition (xid, ann, _, te, ty, _) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             print_term te ;
-             print_term ty
-          >]
-       | C.AAxiom (xid, ann, _, ty, _) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             print_term ty
-          >]
-       | C.AVariable (xid, ann, _, bo, ty) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             (match bo with
-                 None -> [<>]
-               | Some bo -> print_term bo
-             ) ;
-             print_term ty
-          >]
-       | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             List.fold_right
-              (fun (_,t) i -> [< print_term t ; i >])
-              conjs [<>] ;
-             print_term bo ;
-             print_term ty
-          >]
-       | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
-          [< (match !ann with
-                 None -> [<>]
-               | Some ann ->
-                  X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
-             ) ;
-             List.fold_right
-              (fun x i -> [< print_mutual_inductive_type x ; i >])
-              tys [< >]
-          >]
-      end
-  >]
-;;