]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/lexicon/lexiconEngine.ml
Huge commit with several changes:
[helm.git] / helm / software / components / lexicon / lexiconEngine.ml
index c86e161357eb9cd136c6a1a0fd9ef8aa6c37835b..805da25c8e53c18340649fcbd6ead78db3b6fdde 100644 (file)
@@ -120,12 +120,15 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd =
           ->
            let item = DisambiguateTypes.Id id in
             begin try
-              let uri =
-               match DisambiguateTypes.Environment.find item status.aliases with
-                  L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
-                | _ -> assert false
-              in
-               CicNotationPt.UriPattern uri
+              match DisambiguateTypes.Environment.find item status.aliases with
+                 L.Ident_alias (_, uri) ->
+                  (try
+                    CicNotationPt.NRefPattern
+                     (NReference.reference_of_string uri)
+                   with
+                    NReference.IllFormedReference _ ->
+                     CicNotationPt.UriPattern (UriManager.uri_of_string uri))
+               | _ -> assert false
              with Not_found -> 
               prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ 
                (DisambiguateTypes.string_of_domain_item item));