X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=0dd5c0885e7a1ce6636cd6d765c4fb530b1d5e21;hb=2fb7dd29bac6ee7add3618c5d798fa60ab0c8eb4;hp=b9f6d388fa2faa50c318383f373b322b0bde459b;hpb=fd4196b476bff30c46a80cd858ea7bf057f301eb;p=helm.git

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