+
+(* 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;;
[< 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 [<>])
["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" ;