From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Nov 2005 12:18:19 +0000 (+0000)
Subject: Implicit aliases are now defined as all the aliases whose baseuri is the
X-Git-Tag: make_still_working~8063
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06dbe094092da9e14a1719958d7a475da5e05aea;p=helm.git

Implicit aliases are now defined as all the aliases whose baseuri is the
baseuri of the current development. Much much cleaner.
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 49c3046b8..9b9e87085 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -126,13 +126,14 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
+    let baseuri = MatitaTypes.get_string_option new_status "baseuri" in
     List.fold_left (
       fun (initial_space,status,acc) (k,((v,_) as value)) -> 
-        let b = 
-          try
-            let v = UM.strip_xpointer (UM.uri_of_string v) in
-            List.mem v new_status.objects 
-          with UM.IllFormedUri _ -> false
+        let b =
+         try
+          UM.buri_of_uri (UM.uri_of_string v) = baseuri
+         with
+          UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
         in
         if b then 
           initial_space,status,acc