From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 2 Sep 2008 13:59:47 +0000 (+0000)
Subject: Uri ending in '' were not accepted. Fixed.
X-Git-Tag: make_still_working~4827
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e79f902b0fea9afb02576b653b384bc512b2264;p=helm.git

Uri ending in '' were not accepted. Fixed.
---

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index b9f6d388f..0dd5c0885 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -537,7 +537,8 @@ EXTEND
       let alpha = "[a-zA-Z]" in
       let num = "[0-9]+" in
       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
-      let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+      let decoration = "\\'" in
+      let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
       let rex = Str.regexp ("^"^ident^"$") in
       if Str.string_match rex id 0 then
         if (try ignore (UriManager.uri_of_string uri); true