From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Nov 2010 20:54:55 +0000 (+0000)
Subject: Minor code clean-up to simplify module dependencies.
X-Git-Tag: make_still_working~2732
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8161bcb58808e60658072bc3da83b62d1df2a223;p=helm.git

Minor code clean-up to simplify module dependencies.
---

diff --git a/matita/components/METAS/meta.helm-content_pres.src b/matita/components/METAS/meta.helm-content_pres.src
index 8db3fca82..f9540fa62 100644
--- a/matita/components/METAS/meta.helm-content_pres.src
+++ b/matita/components/METAS/meta.helm-content_pres.src
@@ -1,4 +1,4 @@
-requires="helm-content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
+requires="helm-content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
 version="0.0.1"
 archive(byte)="content_pres.cma"
 archive(native)="content_pres.cmxa"
diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml
index 5f9f202ca..d3465d30a 100644
--- a/matita/components/content_pres/cicNotationPres.ml
+++ b/matita/components/content_pres/cicNotationPres.ml
@@ -200,13 +200,6 @@ let add_parens child_prec curr_prec t =
       BoxPp.render_to_string (function x::_->x|_->assert false)
         ~map_unicode_to_tex:false 80 t);*)t)
 
-let lookup_uri ids_to_uris id =
- try
-   let uri = Hashtbl.find ids_to_uris id in
-   Some (NReference.string_of_reference uri)
- with Not_found -> None
-;;
-
 let render ~lookup_uri ?(prec=(-1)) =
   let module A = Ast in
   let module P = Mpresentation in
diff --git a/matita/components/content_pres/cicNotationPres.mli b/matita/components/content_pres/cicNotationPres.mli
index ce8ee1ca6..a558da866 100644
--- a/matita/components/content_pres/cicNotationPres.mli
+++ b/matita/components/content_pres/cicNotationPres.mli
@@ -35,14 +35,11 @@ val box_of_mpres: mathml_markup -> boxml_markup
 
 (** {2 Rendering} *)
 
-val lookup_uri: (Interpretations.cic_id,NReference.reference) Hashtbl.t ->
-  Interpretations.cic_id -> string option
-
 (** level 1 -> level 0
  * @param ids_to_uris mapping id -> uri for hyperlinking
  * @param prec precedence level *)
 val render:
- lookup_uri:(Interpretations.cic_id -> string option) -> ?prec:int -> NotationPt.term ->
+ lookup_uri:(Content.id -> string option) -> ?prec:int -> NotationPt.term ->
   markup
 
 (** level 0 -> xml stream *)
diff --git a/matita/components/content_pres/content2pres.mli b/matita/components/content_pres/content2pres.mli
index 87843815f..52ce9ad5a 100644
--- a/matita/components/content_pres/content2pres.mli
+++ b/matita/components/content_pres/content2pres.mli
@@ -35,6 +35,6 @@
 val ncontent2pres:
  #TermContentPres.status ->
   ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool ->
-  ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t ->
+  ids_to_nrefs:(Content.id, NReference.reference) Hashtbl.t ->
   NotationPt.term Content.cobj ->
     CicNotationPres.boxml_markup
diff --git a/matita/components/content_pres/sequent2pres.mli b/matita/components/content_pres/sequent2pres.mli
index ae1051490..a81872159 100644
--- a/matita/components/content_pres/sequent2pres.mli
+++ b/matita/components/content_pres/sequent2pres.mli
@@ -34,6 +34,6 @@
 
 val nsequent2pres :
  #TermContentPres.status ->
- ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t ->
+ ids_to_nrefs:(Content.id, NReference.reference) Hashtbl.t ->
  subst:NCic.substitution -> NotationPt.term Content.conjecture ->
   CicNotationPres.boxml_markup
diff --git a/matita/components/ng_cic_content/interpretations.mli b/matita/components/ng_cic_content/interpretations.mli
index a4a3fb9c0..4b9fdae76 100644
--- a/matita/components/ng_cic_content/interpretations.mli
+++ b/matita/components/ng_cic_content/interpretations.mli
@@ -26,8 +26,6 @@
 
   (** {2 State handling} *)
 
-type id = string
-
 val hide_coercions: bool ref
 
 type db
@@ -46,8 +44,6 @@ class status :
     method set_interp_status: #g_status -> 'self
   end
 
-type cic_id = string
-
 val add_interpretation:
   #status as 'status ->
   string ->                                       (* id / description *)
@@ -83,9 +79,9 @@ val nmap_sequent:
  #status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   int * NCic.conjecture ->
    NotationPt.term Content.conjecture *
-    (id, NReference.reference) Hashtbl.t    (* id -> reference *)
+    (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
 
 val nmap_obj:
  #status -> NCic.obj ->
   NotationPt.term Content.cobj *
-   (id, NReference.reference) Hashtbl.t    (* id -> reference *)
+   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)