* the regular expressions must have $ otherwise the shortest match

  will be found first and the annotations will never show up

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index ac8b98305b2c392450da5fe3629a9c6d30284f2e..366c233b4979804322f4a83a1d03613a91312dfa 100644 (file)
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -152,13 +152,13 @@ let return_ls =
   in
   let basepart_RE =
     Pcre.regexp
-      "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?"
+      "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
   let (types_RE, types_ann_RE, body_RE, body_ann_RE,
        proof_tree_RE, proof_tree_ann_RE) =
-    (Pcre.regexp "\\.types", Pcre.regexp "\\.types\\.ann",
-     Pcre.regexp "\\.body", Pcre.regexp "\\.body.ann",
-     Pcre.regexp "\\.proof_tree", Pcre.regexp "\\.proof_tree\\.ann")
+    (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
+     Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
+     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")