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 8db3fca82b66cfa262b035ba564d216a6c02fa6b..f9540fa62e0bb230e1d8bbd0b43eea407aa85e08 100644 (file)
--- 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 5f9f202caeaf09b8d7b299444018106abe8a6062..d3465d30a4e21d46b903f70ac0afa67df7c6990f 100644 (file)
--- 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 ce8ee1ca6b10dfcc5640ba3396090db46915c16e..a558da86622ee92cf62b1928834efbd63b4b157c 100644 (file)
--- 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 87843815fb54b5c8b29638e8a4a50f2d6bccce5e..52ce9ad5aacacff3186873c72e8bde3af9e4ac36 100644 (file)
--- 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 ae10514902f914c17cb3f11964eb56a4d7485b2d..a81872159928780c45b1599d8ffe28838533d220 100644 (file)
--- 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 a4a3fb9c09af03ae8cdfbaeb2f4be865aa52fabd..4b9fdae768c7e64385dbb71996535fce907a2795 100644 (file)
--- 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 *)