From 06dbe094092da9e14a1719958d7a475da5e05aea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 12:18:19 +0000 Subject: [PATCH] Implicit aliases are now defined as all the aliases whose baseuri is the baseuri of the current development. Much much cleaner. --- helm/matita/matitaScript.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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 -- 2.39.2