From 8d1b8c31da7bdfb695636bd4ef1c7c948ce511c4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Sep 2002 10:03:24 +0000 Subject: [PATCH] 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). --- helm/gTopLevel/mQueryGenerator.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) 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; -- 2.39.2