From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Sep 2002 10:03:24 +0000 (+0000)
Subject: Patch applied to the locate query: when used to retrieve the first inductive
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d1b8c31da7bdfb695636bd4ef1c7c948ce511c4;p=helm.git

Patch applied to the locate query: when used to retrieve the first inductive
type of a mutual inductive types block, the returned URI is now the URI of
the type (with the fragment identifier!) and not the one of the block (without).
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 5c6fb27d7..9dd40336a 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -220,8 +220,21 @@ let locate_query s =
                        )
              )
 
-let locate s = Mqint.execute (locate_query s)
-let locate_html s = build_result (locate_query s)
+let locate s =
+ (*CSC: the code should be: Mqint.execute (locate_query s)                  *)
+ (*CSC: what follows is the patch to map mutual inductive definition blocks *)
+ (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first  *)
+ (*CSC: mutual inductive type of their block.                               *)
+ let MQRefs uris = Mqint.execute (locate_query s) in
+  MQRefs
+   (List.map
+    (function uri ->
+      if String.sub uri (String.length uri - 4) 4 = ".con" then uri else
+       uri ^ "#1/1"
+    ) uris)
+;;
+
+let locate_html s = build_result (locate_query s);;
 
 let levels e c t =
    env := e; cont := c;