]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
more abstract discrimination tree
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index 38a8667d304ae511da33b6abf47971f178922726..0dd5c0885e7a1ce6636cd6d765c4fb530b1d5e21 100644 (file)
@@ -509,7 +509,7 @@ EXTEND
     | [ IDENT "inline"]; 
         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
         suri = QSTRING; prefix = OPT QSTRING;
-       flavour = OPT [ IDENT "as"; attr = inline_flavour -> attr ]->
+       flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
          let style = match style with 
             | None       -> GrafiteAst.Declarative
             | Some depth -> GrafiteAst.Procedural depth
@@ -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