]> 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 6f30801a4b1c284d5ee6758e1bd02678217d2268..805da25c8e53c18340649fcbd6ead78db3b6fdde 100644 (file)
@@ -27,7 +27,7 @@
 
 module L = LexiconAst
 
-let debug = ref true
+let debug = ref false
 
 (* lexicon file name * ma file name *)
 exception IncludedFileNotCompiled of string * string 
@@ -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));