X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fcic2Xml.ml;h=58f35bb6f687c0581bd611589ac9ee94f3e25d97;hb=fde0ad77237a2fbdfb5621d5b5085fe7c82e3f92;hp=ff16e2f701f168deff3e8259ecbd6e8555c6c8d9;hpb=c01d2aaea05f7385bee46addd900cd0397756389;p=helm.git

diff --git a/helm/interface/cic2Xml.ml b/helm/interface/cic2Xml.ml
index ff16e2f70..58f35bb6f 100644
--- a/helm/interface/cic2Xml.ml
+++ b/helm/interface/cic2Xml.ml
@@ -1,3 +1,29 @@
+
+(* 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;;
@@ -59,6 +85,13 @@ let print_term curi =
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" ["binder",id] (aux t)
         >]
+     | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+       assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+     | C.ALetIn (xid,_,C.Name id,s,t) ->
+       X.xml_nempty "LETIN" ["id",xid]
+        [< X.xml_nempty "term" [] (aux s) ;
+           X.xml_nempty "letintarget" ["binder",id] (aux t)
+        >]
      | C.AAppl (id,_,li) ->
         X.xml_nempty "APPLY" ["id",id]
          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
@@ -175,11 +208,16 @@ let pp obj curi =
           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
           [< X.xml_nempty "type" [] (print_term curi ty) >]
       >]
-   | C.AVariable (xid, _, name, ty) ->
+   | C.AVariable (xid, _, name, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
          X.xml_nempty "Variable" ["name",name ; "id",xid]
-          [< X.xml_nempty "type" [] (print_term curi ty) >]
+          [< (match bo with
+                 None -> [<>]
+               | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
+             ) ;
+             X.xml_nempty "type" [] (print_term curi ty)
+          >]
       >]
    | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;