Initial revision

[helm.git] / helm / gTopLevel / sequentPp.ml

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index bffb3030c27cc81b76693b7e1d83c3221697f3e0..d0430162e848951e2a692e9dd7008f52c41c270c 100644 (file)
--- a/helm/gTopLevel/sequentPp.ml
+++ b/helm/gTopLevel/sequentPp.ml
@@ -1,3 +1,28 @@
+(* 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/.
+ *)
+
 module TextualPp =
  struct
   (* It also returns the pretty-printing context! *)
@@ -43,6 +68,8 @@ module XmlPp =
     let ids_to_father_ids = Hashtbl.create 503 in
     let ids_to_inner_sorts = Hashtbl.create 503 in
     let ids_to_inner_types = Hashtbl.create 503 in
+    let ids_to_hypotheses = Hashtbl.create 11 in
+    let hypotheses_seed = ref 0 in
     let seed = ref 0 in
      let acic_of_cic_context =
       Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
@@ -51,31 +78,35 @@ module XmlPp =
       let final_s,_ =
        (List.fold_right
          (fun binding (s,context) ->
-           match binding with
-              (Some (n,(Cic.Def t as b)) as entry)
-            | (Some (n,(Cic.Decl t as b)) as entry) ->
-               let acic = acic_of_cic_context context t in
-                [< s ;
-                   X.xml_nempty
-                    (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
-                    ["name",(match n with Cic.Name n -> n | _ -> assert false)]
-                    (Cic2Xml.print_term
-                      (UriManager.uri_of_string "cic:/dummy.con")
-                      ids_to_inner_sorts acic)
-                >], (entry::context)
-            | None ->
-               [< s ; X.xml_empty "Hidden" [] >], (None::context)
+           let hid = "h" ^ string_of_int !hypotheses_seed in
+            Hashtbl.add ids_to_hypotheses hid binding ;
+            incr hypotheses_seed ;
+            match binding with
+               (Some (n,(Cic.Def t as b)) as entry)
+             | (Some (n,(Cic.Decl t as b)) as entry) ->
+                let acic = acic_of_cic_context context t None in
+                 [< s ;
+                    X.xml_nempty
+                     (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
+                     ["name",(match n with Cic.Name n -> n | _ -> assert false);
+                      "id",hid]
+                     (Cic2Xml.print_term
+                       (UriManager.uri_of_string "cic:/dummy.con")
+                       ~ids_to_inner_sorts acic)
+                 >], (entry::context)
+             | None ->
+                [< s ; X.xml_empty "Hidden" [] >], (None::context)
          ) context ([<>],[])
        )
       in
-       let acic = acic_of_cic_context context goal in
+       let acic = acic_of_cic_context context goal None in
         X.xml_nempty "Sequent" ["no",string_of_int metano]
          [< final_s ;
             Xml.xml_nempty "Goal" []
              (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
-               ids_to_inner_sorts acic)
+               ~ids_to_inner_sorts acic)
          >],
-         ids_to_terms,ids_to_father_ids
+         ids_to_terms,ids_to_father_ids,ids_to_hypotheses
   ;;
  end
 ;;