From f6b7c6ae353e014761a3d24dbc87e00d828d7f2d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 26 Oct 2010 14:32:14 +0000 Subject: [PATCH] urimanager removed --- matita/components/METAS/meta.helm-getter.src | 2 +- .../components/METAS/meta.helm-urimanager.src | 5 - matita/components/Makefile | 4 +- matita/components/content/content.ml | 1 - matita/components/content/content.mli | 1 - matita/components/content/interpretations.ml | 5 +- matita/components/content/interpretations.mli | 1 - matita/components/content/notationPp.ml | 5 +- matita/components/content/notationPt.ml | 3 +- matita/components/content/notationUtil.ml | 12 +- matita/components/content/notationUtil.mli | 3 +- .../content_pres/cicNotationPres.ml | 2 +- .../content_pres/cicNotationPres.mli | 2 +- .../components/content_pres/content2pres.ml | 24 +- .../content_pres/termContentPres.ml | 2 +- .../components/disambiguation/disambiguate.ml | 1 - .../disambiguation/disambiguateTypes.ml | 6 +- .../disambiguation/disambiguateTypes.mli | 6 +- matita/components/getter/http_getter.ml | 13 +- matita/components/getter/http_getter.mli | 8 +- matita/components/grafite/grafiteMarshal.ml | 2 - .../grafite_engine/grafiteEngine.ml | 36 +-- .../grafite_engine/grafiteEngine.mli | 2 +- .../grafite_engine/nCicCoercDeclaration.ml | 4 +- .../grafite_engine/nCicCoercDeclaration.mli | 4 +- .../grafite_parser/dependenciesParser.ml | 13 +- .../grafite_parser/dependenciesParser.mli | 2 +- .../grafite_parser/grafiteDisambiguate.ml | 1 - .../grafite_parser/grafiteParser.ml | 7 +- matita/components/lexicon/lexiconEngine.ml | 7 +- matita/components/lexicon/lexiconMarshal.ml | 4 - matita/components/lexicon/lexiconSync.ml | 57 +--- matita/components/lexicon/lexiconSync.mli | 3 +- matita/components/library/libraryClean.ml | 8 +- .../ng_cic_content/nTermCicContent.ml | 8 +- .../ng_cic_content/ncic2astMatcher.ml | 5 - .../ng_cic_content/ncic2astMatcher.mli | 2 - .../ng_disambiguation/disambiguateChoices.ml | 8 +- .../ng_disambiguation/disambiguateChoices.mli | 2 - .../ng_disambiguation/nCicDisambiguate.ml | 6 +- .../ng_disambiguation/nCicDisambiguate.mli | 2 - matita/components/urimanager/.depend | 3 - matita/components/urimanager/.depend.opt | 3 - matita/components/urimanager/Makefile | 10 - matita/components/urimanager/uriManager.ml | 264 ------------------ matita/components/urimanager/uriManager.mli | 75 ----- matita/matita/matita.glade | 7 - matita/matita/matita.ml | 10 +- matita/matita/matitaExcPp.ml | 1 - matita/matita/matitaGui.ml | 13 +- matita/matita/matitaGui.mli | 2 +- matita/matita/matitaMathView.ml | 28 +- matita/matita/matitaScript.ml | 2 +- matita/matita/matitaScript.mli | 2 +- matita/matita/matitaTypes.ml | 6 +- matita/matita/matitaTypes.mli | 4 +- matita/matita/matitaclean.ml | 10 +- matita/matita/matitadep.ml | 5 +- 58 files changed, 117 insertions(+), 617 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-urimanager.src delete mode 100644 matita/components/urimanager/.depend delete mode 100644 matita/components/urimanager/.depend.opt delete mode 100644 matita/components/urimanager/Makefile delete mode 100644 matita/components/urimanager/uriManager.ml delete mode 100644 matita/components/urimanager/uriManager.mli diff --git a/matita/components/METAS/meta.helm-getter.src b/matita/components/METAS/meta.helm-getter.src index 8a7badf74..b060fb62a 100644 --- a/matita/components/METAS/meta.helm-getter.src +++ b/matita/components/METAS/meta.helm-getter.src @@ -1,4 +1,4 @@ -requires="http unix pcre zip helm-xml helm-logger helm-urimanager helm-registry" +requires="http unix pcre zip helm-xml helm-logger helm-ng_kernel helm-registry" version="0.0.1" archive(byte)="getter.cma" archive(native)="getter.cmxa" diff --git a/matita/components/METAS/meta.helm-urimanager.src b/matita/components/METAS/meta.helm-urimanager.src deleted file mode 100644 index ff1874688..000000000 --- a/matita/components/METAS/meta.helm-urimanager.src +++ /dev/null @@ -1,5 +0,0 @@ -requires="str" -version="0.0.1" -archive(byte)="urimanager.cma" -archive(native)="urimanager.cmxa" -linkopts="" diff --git a/matita/components/Makefile b/matita/components/Makefile index 3f3b5dea9..7d463f88c 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -11,15 +11,13 @@ MODULES = \ registry \ syntax_extensions \ thread \ - urimanager \ logger \ + ng_kernel \ getter \ library \ - ng_kernel \ content \ grafite \ disambiguation \ - ng_kernel \ ng_refiner \ ng_disambiguation \ ng_cic_content \ diff --git a/matita/components/content/content.ml b/matita/components/content/content.ml index 1e4cc88af..6a23ab1e7 100644 --- a/matita/components/content/content.ml +++ b/matita/components/content/content.ml @@ -164,7 +164,6 @@ type 'term in_object_context_element = type 'term cobj = id * (* id *) - UriManager.uri list * (* params *) 'term conjecture list option * (* optional metasenv *) 'term in_object_context_element (* actual object *) ;; diff --git a/matita/components/content/content.mli b/matita/components/content/content.mli index 229d30749..dfd732ebd 100644 --- a/matita/components/content/content.mli +++ b/matita/components/content/content.mli @@ -152,7 +152,6 @@ type 'term in_object_context_element = type 'term cobj = id * (* id *) - UriManager.uri list * (* params *) 'term conjecture list option * (* optional metasenv *) 'term in_object_context_element (* actual object *) ;; diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index 8059eeaae..7e85d0fc1 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -40,7 +40,7 @@ type cic_id = string type term_info = { sort: (cic_id, Ast.sort_kind) Hashtbl.t; - uri: (cic_id, UriManager.uri) Hashtbl.t; + uri: (cic_id, NReference.reference) Hashtbl.t; } (* persistent state *) @@ -188,7 +188,7 @@ let remove_interpretation id = let init () = List.iter (fun f -> f []) !load_patterns32s let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern + ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern = let lookup name = try List.assoc name env @@ -197,7 +197,6 @@ let instantiate_appl_pattern assert false in let rec aux = function - | Ast.UriPattern uri -> term_of_uri uri | Ast.NRefPattern nref -> term_of_nref nref | Ast.ImplicitPattern -> mk_implicit false | Ast.VarPattern name -> lookup name diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli index 10a2f093e..50432801d 100644 --- a/matita/components/content/interpretations.mli +++ b/matita/components/content/interpretations.mli @@ -60,7 +60,6 @@ val set_active_interpretations: interpretation_id list -> unit val instantiate_appl_pattern: mk_appl:('term list -> 'term) -> mk_implicit:(bool -> 'term) -> - term_of_uri : (UriManager.uri -> 'term) -> term_of_nref : (NReference.reference -> 'term) -> (string * 'term) list -> NotationPt.cic_appl_pattern -> 'term diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index 59df4ffdd..e9209d515 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -104,7 +104,7 @@ let rec pp_term ?(pp_parens = true) t = sprintf " in %s%s" ty (match debug_printing, href_opt with | true, Some uri -> - sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "")) (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (pp_patterns patterns) @@ -183,7 +183,7 @@ and pp_pattern = let head_pp = head ^ (match debug_printing, href with - | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "") in sprintf "%s \\Rightarrow %s" @@ -347,7 +347,6 @@ let pp_env env = env) let rec pp_cic_appl_pattern = function - | Ast.UriPattern uri -> UriManager.string_of_uri uri | Ast.NRefPattern nref -> NReference.string_of_reference nref | Ast.VarPattern name -> name | Ast.ImplicitPattern -> "?" diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index aa83b20f3..cead5e7ae 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -37,7 +37,7 @@ let fail floc msg = let (x, y) = HExtlib.loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) -type href = UriManager.uri +type href = NReference.reference type child_pos = [ `Left | `Right | `Inner ] @@ -165,7 +165,6 @@ type argument_pattern = | IdentArg of int * string (* eta-depth, name *) type cic_appl_pattern = - | UriPattern of UriManager.uri | NRefPattern of NReference.reference | VarPattern of string | ImplicitPattern diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 52abe4564..98e1ba663 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -328,21 +328,13 @@ let dressn ~sep:sauces = let find_appl_pattern_uris ap = let rec aux acc = function - | Ast.UriPattern uri -> `Uri uri :: acc - | Ast.NRefPattern nref -> `NRef nref :: acc + | Ast.NRefPattern nref -> nref :: acc | Ast.ImplicitPattern | Ast.VarPattern _ -> acc | Ast.ApplPattern apl -> List.fold_left aux acc apl in let uris = aux [] ap in - let cmp u1 u2 = - match u1,u2 with - `Uri u1, `Uri u2 -> UriManager.compare u1 u2 - | `NRef r1, `NRef r2 -> NReference.compare r1 r2 - | `Uri _,`NRef _ -> -1 - | `NRef _, `Uri _ -> 1 - in - HExtlib.list_uniq (List.fast_sort cmp uris) + HExtlib.list_uniq (List.fast_sort NReference.compare uris) let rec find_branch = function diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli index daca93587..f7c1c0cd4 100644 --- a/matita/components/content/notationUtil.mli +++ b/matita/components/content/notationUtil.mli @@ -76,8 +76,7 @@ val group: NotationPt.term list -> NotationPt.term val ungroup: NotationPt.term list -> NotationPt.term list val find_appl_pattern_uris: - NotationPt.cic_appl_pattern -> - [`Uri of UriManager.uri | `NRef of NReference.reference] list + NotationPt.cic_appl_pattern -> NReference.reference list val find_branch: NotationPt.term -> NotationPt.term diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml index 26370ff22..5f9f202ca 100644 --- a/matita/components/content_pres/cicNotationPres.ml +++ b/matita/components/content_pres/cicNotationPres.ml @@ -203,7 +203,7 @@ let add_parens child_prec curr_prec t = let lookup_uri ids_to_uris id = try let uri = Hashtbl.find ids_to_uris id in - Some (UriManager.string_of_uri uri) + Some (NReference.string_of_reference uri) with Not_found -> None ;; diff --git a/matita/components/content_pres/cicNotationPres.mli b/matita/components/content_pres/cicNotationPres.mli index 5961b8887..ce8ee1ca6 100644 --- a/matita/components/content_pres/cicNotationPres.mli +++ b/matita/components/content_pres/cicNotationPres.mli @@ -35,7 +35,7 @@ val box_of_mpres: mathml_markup -> boxml_markup (** {2 Rendering} *) -val lookup_uri: (Interpretations.cic_id,UriManager.uri) Hashtbl.t -> +val lookup_uri: (Interpretations.cic_id,NReference.reference) Hashtbl.t -> Interpretations.cic_id -> string option (** level 1 -> level 0 diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index cd2e62c21..f869801f9 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -881,22 +881,6 @@ let metasenv2pres term2pres = function (let _ = incr counter; in (string_of_int !counter)))) :: (List.map (conjecture2pres term2pres) metasenv'))] -let params2pres params = - let param2pres uri = - B.b_text [Some "xlink", "href", UriManager.string_of_uri uri] - (UriManager.name_of_uri uri) - in - let rec spatiate = function - | [] -> [] - | hd :: [] -> [hd] - | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl - in - match params with - | [] -> [] - | p -> - let params = spatiate (List.map param2pres p) in - [B.b_space; - B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])] let inductive2pres term2pres ind = let constructor2pres decl = B.b_h [] [ @@ -994,7 +978,7 @@ let njoint_def2pres term2pres joint_kind defs = let ncontent2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres - (id,params,metasenv,obj : NotationPt.term Content.cobj) + (id,metasenv,obj : NotationPt.term Content.cobj) = match obj with | `Def (Content.Const, thesis, `Proof p) -> @@ -1006,7 +990,7 @@ let ncontent2pres0 B.b_v [Some "helm","xref","id"] ([ B.b_h [] (B.b_kw ("ntheorem " ^ name) :: - params2pres params @ [B.b_kw ":"]); + [B.b_kw ":"]); B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @ metasenv2pres term2pres metasenv @ [proof ; B.b_kw "qed."]) @@ -1015,7 +999,7 @@ let ncontent2pres0 B.b_v [Some "helm","xref","id"] ([B.b_h [] - (B.b_kw ("ndefinition " ^ name) :: params2pres params @ [B.b_kw ":"]); + (B.b_kw ("ndefinition " ^ name) :: [B.b_kw ":"]); B.indent (term2pres ty)] @ metasenv2pres term2pres metasenv @ [B.b_kw ":="; @@ -1026,7 +1010,7 @@ let ncontent2pres0 let name = get_name decl.Content.dec_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: params2pres params); + ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: []); B.b_kw "Type:"; B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 28bcbe314..80d4d65a9 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -81,7 +81,7 @@ let ident_w_href href i = match href with | None -> ident i | Some href -> - let href = UriManager.string_of_uri href in + let href = NReference.string_of_reference href in add_xml_attrs [Some "xlink", "href", href] (ident i) let binder_symbol s = diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 0e4636d57..8be47f063 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -28,7 +28,6 @@ open Printf open DisambiguateTypes -open UriManager module Ast = NotationPt diff --git a/matita/components/disambiguation/disambiguateTypes.ml b/matita/components/disambiguation/disambiguateTypes.ml index 23c16cff2..f6e03d098 100644 --- a/matita/components/disambiguation/disambiguateTypes.ml +++ b/matita/components/disambiguation/disambiguateTypes.ml @@ -73,14 +73,14 @@ type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list + title:string -> msg:string -> id:string -> NReference.reference list -> + NReference.reference list type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list type input_or_locate_uri_type = - title:string -> ?id:string -> unit -> UriManager.uri option + title:string -> ?id:string -> unit -> NReference.reference option let string_of_domain_item = function | Id s -> Printf.sprintf "ID(%s)" s diff --git a/matita/components/disambiguation/disambiguateTypes.mli b/matita/components/disambiguation/disambiguateTypes.mli index c3601eae5..1e99fd404 100644 --- a/matita/components/disambiguation/disambiguateTypes.mli +++ b/matita/components/disambiguation/disambiguateTypes.mli @@ -48,13 +48,13 @@ type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list + title:string -> msg:string -> id:string -> NReference.reference list -> + NReference.reference list type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list type input_or_locate_uri_type = - title:string -> ?id:string -> unit -> UriManager.uri option + title:string -> ?id:string -> unit -> NReference.reference option val string_of_domain_item: domain_item -> string diff --git a/matita/components/getter/http_getter.ml b/matita/components/getter/http_getter.ml index b41c4788f..4e431ee81 100644 --- a/matita/components/getter/http_getter.ml +++ b/matita/components/getter/http_getter.ml @@ -151,10 +151,7 @@ let exists ~local uri = let uri = deref_index_theory ~local uri in Http_getter_storage.exists ~local (uri ^ xml_suffix) -let is_an_obj s = - try - s <> UriManager.buri_of_uri (UriManager.uri_of_string s) - with UriManager.IllFormedUri _ -> true +let is_an_obj s = s <> NUri.baseuri_of_uri (NUri.uri_of_string s) let resolve ~local ~writable uri = if remote () then @@ -363,13 +360,13 @@ let getalluris () = (* Shorthands from now on *) -let getxml' uri = getxml (UriManager.string_of_uri uri) +let getxml' uri = getxml (NUri.string_of_uri uri) let resolve' ~local ~writable uri = - resolve ~local ~writable (UriManager.string_of_uri uri) + resolve ~local ~writable (NUri.string_of_uri uri) ;; -let exists' ~local uri = exists ~local (UriManager.string_of_uri uri) +let exists' ~local uri = exists ~local (NUri.string_of_uri uri) let filename' ~local ~writable uri = - filename ~local ~writable (UriManager.string_of_uri uri) + filename ~local ~writable (NUri.string_of_uri uri) ;; let tilde_expand_key k = diff --git a/matita/components/getter/http_getter.mli b/matita/components/getter/http_getter.mli index 5cf5cd38e..3b8ebb9cb 100644 --- a/matita/components/getter/http_getter.mli +++ b/matita/components/getter/http_getter.mli @@ -60,10 +60,10 @@ val ls: local:bool -> string -> ls_item list (** {2 UriManager shorthands} *) -val getxml' : UriManager.uri -> string -val resolve' : local:bool -> writable:bool -> UriManager.uri -> string -val exists' : local:bool -> UriManager.uri -> bool -val filename' : local:bool -> writable:bool -> UriManager.uri -> string +val getxml' : NUri.uri -> string +val resolve' : local:bool -> writable:bool -> NUri.uri -> string +val exists' : local:bool -> NUri.uri -> bool +val filename' : local:bool -> writable:bool -> NUri.uri -> string (** {2 Misc} *) diff --git a/matita/components/grafite/grafiteMarshal.ml b/matita/components/grafite/grafiteMarshal.ml index 327f39809..d18ee2f0c 100644 --- a/matita/components/grafite/grafiteMarshal.ml +++ b/matita/components/grafite/grafiteMarshal.ml @@ -38,8 +38,6 @@ let load_moo_from_file ~fname = (raw: moo) let rehash_cmd_uris = - let rehash_uri uri = - UriManager.uri_of_string (UriManager.string_of_uri uri) in function | GrafiteAst.Include _ as cmd -> cmd | cmd -> diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 055059dd7..22f14db13 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -36,12 +36,6 @@ type options = { do_heavy_checks: bool ; } -let concat_nuris uris nuris = - match uris,nuris with - | `New uris, `New nuris -> `New (nuris@uris) - | _ -> assert false -;; - let basic_eval_unification_hint (t,n) status = NCicUnifHint.add_user_provided_hint status t n ;; @@ -67,7 +61,7 @@ let eval_unification_hint status t n = let status = basic_eval_unification_hint (t,n) status in let dump = inject_unification_hint (t,n)::status#dump in let status = status#set_dump dump in - status,`New [] + status,[] ;; let basic_index_obj l status = @@ -216,7 +210,7 @@ let eval_add_constraint status u1 u2 = let status = basic_eval_add_constraint (u1,u2) status in let dump = inject_constraint (u1,u2)::status#dump in let status = status#set_dump dump in - status,`New [] + status,[] ;; let eval_ng_tac tac = @@ -385,7 +379,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let uris = uri::List.rev uris_rev in *) let status = status#set_ng_mode `CommandMode in - let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in + let status = LexiconSync.add_aliases_for_objs status [uri] in let status,uris = List.fold_left (fun (status,uris) boxml -> @@ -400,13 +394,13 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = status, uris end else - nstatus, concat_nuris uris nuris + nstatus, uris@nuris with | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> (*HLog.warn "error in generating projection/eliminator";*) status,uris - ) (status,`New [] (* uris *)) boxml in + ) (status,[] (* uris *)) boxml in let _,_,_,_,nobj = obj in let status = match nobj with NCic.Inductive (is_ind,leftno,[it],_) -> @@ -423,7 +417,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let _,_,menv,_,_ = invobj in fst (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New [])) + | _ -> status,[])) (* XXX *) with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) @@ -454,7 +448,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) in - let uris = concat_nuris nuris uris in + let uris = nuris@uris in status, uris with MultiPassDisambiguator.DisambiguationError _-> HLog.warn ("error in generating coercion: "^name); @@ -513,7 +507,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (match nmenv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New []) + | _ -> status,[]) | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -531,7 +525,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> prerr_endline ("Discriminator: non empty metasenv"); - status, `New []) *) + status, []) *) | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -568,7 +562,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = ;; let eval_comment ~disambiguate_command opts status (text,prefix_len,c) = - status, `New [] + status, [] let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = let status,cmd = disambiguate_command status (text,prefix_len,cmd) in @@ -595,9 +589,9 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = GrafiteTypes.add_moo_content [GrafiteAst.Include (loc,baseuri)] status in - status,`New [] - | GrafiteAst.Print (_,_) -> status,`New [] - | GrafiteAst.Set (loc, name, value) -> status, `New [] + status,[] + | GrafiteAst.Print (_,_) -> status,[] + | GrafiteAst.Set (loc, name, value) -> status, [] in status,uris @@ -614,7 +608,7 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = subst_metasenv_and_fix_names status) status tacl in - status,`New [] + status,[] | GrafiteAst.Command (_, cmd) -> eval_command ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.NCommand (_, cmd) -> @@ -636,7 +630,7 @@ and eval_from_moo status fname = eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) status ast in - assert (lemmas=`New []); + assert (lemmas=[]); status) status moo diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index 334488dd3..a6b9d7b1d 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -39,4 +39,4 @@ val eval_ast : GrafiteTypes.status -> GrafiteAst.statement disambiguator_input -> (* the new status and generated objects, if any *) - GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] + GrafiteTypes.status * NUri.uri list diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index 7fcd6a473..3cf076265 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -311,7 +311,7 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity let status, uris = basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status in - status,`New uris + status,uris ;; let eval_ncoercion status name t ty (id,src) tgt = @@ -330,6 +330,6 @@ let eval_ncoercion status name t ty (id,src) tgt = let status, uris = basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status in - status,`New uris + status,uris ;; diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli index 1c9062fd6..9bca1143d 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.mli +++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli @@ -17,12 +17,12 @@ val eval_ncoercion: NotationPt.term -> NotationPt.term -> string * NotationPt.term -> - NotationPt.term -> 'status * [> `New of NUri.uri list ] + NotationPt.term -> 'status * NUri.uri list (* for records, the term is the projection, already refined, while the * first integer is the number of left params and the second integer is * the arity in the `:arity>` syntax *) val basic_eval_and_record_ncoercion_from_t_cpos_arity: #GrafiteTypes.status as 'status -> - string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ] + string * NCic.term * int * int -> 'status * NUri.uri list diff --git a/matita/components/grafite_parser/dependenciesParser.ml b/matita/components/grafite_parser/dependenciesParser.ml index 53fb7ab6d..6b0142bf1 100644 --- a/matita/components/grafite_parser/dependenciesParser.ml +++ b/matita/components/grafite_parser/dependenciesParser.ml @@ -30,12 +30,12 @@ exception UnableToInclude of string (* statements meaningful for matitadep *) type dependency = | IncludeDep of string - | UriDep of UriManager.uri + | UriDep of NUri.uri | InlineDep of string let pp_dependency = function | IncludeDep str -> "include \"" ^ str ^ "\"" - | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\"" + | UriDep uri -> "uri \"" ^ NUri.string_of_uri uri ^ "\"" | InlineDep str -> "inline \"" ^ str ^ "\"" let parse_dependencies lexbuf = @@ -48,12 +48,11 @@ let parse_dependencies lexbuf = (parser | [< '("QSTRING", s) >] -> (* because of alias id qstring = qstring :-( *) - (try - true, (UriDep (UriManager.uri_of_string s) :: acc) - with - UriManager.IllFormedUri _ -> true, acc) + if String.sub s 0 5 <> "cic:/" then true,acc + else + true, (UriDep (NUri.uri_of_string s) :: acc) | [< '("URI", u) >] -> - true, (UriDep (UriManager.uri_of_string u) :: acc) + true, (UriDep (NUri.uri_of_string u) :: acc) | [< '("IDENT", "include"); '("QSTRING", fname) >] -> true, (IncludeDep fname :: acc) | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] -> diff --git a/matita/components/grafite_parser/dependenciesParser.mli b/matita/components/grafite_parser/dependenciesParser.mli index 57529966b..cbdc028dd 100644 --- a/matita/components/grafite_parser/dependenciesParser.mli +++ b/matita/components/grafite_parser/dependenciesParser.mli @@ -28,7 +28,7 @@ exception UnableToInclude of string (* statements meaningful for matitadep *) type dependency = | IncludeDep of string - | UriDep of UriManager.uri + | UriDep of NUri.uri | InlineDep of string val pp_dependency: dependency -> string diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index 8e6631929..c465fe1d8 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -52,7 +52,6 @@ let ncic_mk_choice = function | false -> NCic.Implicit `Term) ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) - ~term_of_uri:(fun _ -> assert false) ~term_of_nref:(fun nref -> NCic.Const nref) name dsc | LexiconAst.Number_alias (_, dsc) -> diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 110c9e912..f0da64a51 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -461,9 +461,7 @@ EXTEND 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 - with UriManager.IllFormedUri _ -> false) || - (try ignore (NReference.reference_of_string uri); true + if (try ignore (NReference.reference_of_string uri); true with NReference.IllFormedReference _ -> false) then L.Ident_alias (id, uri) @@ -532,8 +530,7 @@ EXTEND ] ]; level3_term: [ - [ u = URI -> N.UriPattern (UriManager.uri_of_string u) - | r = NREF -> N.NRefPattern (NReference.reference_of_string r) + [ r = NREF -> N.NRefPattern (NReference.reference_of_string r) | IMPLICIT -> N.ImplicitPattern | id = IDENT -> N.VarPattern id | LPAREN; terms = LIST1 SELF; RPAREN -> diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index 8a5b50354..a0dfb87cf 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -135,12 +135,7 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd = begin try match DisambiguateTypes.Environment.find item status.aliases with L.Ident_alias (_, uri) -> - (try - NotationPt.NRefPattern - (NReference.reference_of_string uri) - with - NReference.IllFormedReference _ -> - NotationPt.UriPattern (UriManager.uri_of_string uri)) + NotationPt.NRefPattern (NReference.reference_of_string uri) | _ -> assert false with Not_found -> prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ diff --git a/matita/components/lexicon/lexiconMarshal.ml b/matita/components/lexicon/lexiconMarshal.ml index 6693de214..5e74e8815 100644 --- a/matita/components/lexicon/lexiconMarshal.ml +++ b/matita/components/lexicon/lexiconMarshal.ml @@ -37,14 +37,10 @@ let load_lexicon_from_file ~fname = (raw: lexicon) let rehash_cmd_uris = - let rehash_uri uri = - UriManager.uri_of_string (UriManager.string_of_uri uri) in function | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) -> let rec aux = function - | NotationPt.UriPattern uri -> - NotationPt.UriPattern (rehash_uri uri) | NotationPt.NRefPattern (NReference.Ref (uri,spec)) -> let uri = NCicLibrary.refresh_uri uri in NotationPt.NRefPattern (NReference.reference_of_spec uri spec) diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml index 33d21a93f..1971ac33e 100644 --- a/matita/components/lexicon/lexiconSync.ml +++ b/matita/components/lexicon/lexiconSync.ml @@ -45,51 +45,20 @@ let alias_diff ~from status = status#lstatus.LexiconEngine.aliases [] ;; -(** given a uri and a type list (the contructors types) builds a list of pairs - * (name,uri) that is used to generate automatic aliases **) -let extract_alias types uri = - fst(List.fold_left ( - fun (acc,i) (name, _, _, cl) -> - (name, UriManager.uri_of_uriref uri i None) :: - (fst(List.fold_left ( - fun (acc,j) (name,_) -> - (((name,UriManager.uri_of_uriref uri i - (Some j)) :: acc) , j+1) - ) (acc,1) cl)),i+1 - ) ([],0) types) - -let build_aliases = - List.map - (fun (name,uri) -> - DisambiguateTypes.Id name, LexiconAst.Ident_alias (name, - UriManager.string_of_uri uri)) - -let add_aliases_for_inductive_def status types uri = - let aliases = build_aliases (extract_alias types uri) in - LexiconEngine.set_proof_aliases status aliases - -let add_alias_for_constant status uri = - let name = UriManager.name_of_uri uri in - let new_env = build_aliases [(name,uri)] in - LexiconEngine.set_proof_aliases status new_env - let add_aliases_for_objs status = - function - `Old _ -> assert false (* MATITA 1.0 *) - | `New nrefs -> - List.fold_left - (fun status nref -> - let references = NCicLibrary.aliases_of nref in - let new_env = - List.map - (fun u -> - let name = NCicPp.r2s true u in - DisambiguateTypes.Id name, - LexiconAst.Ident_alias (name,NReference.string_of_reference u) - ) references - in - LexiconEngine.set_proof_aliases status new_env - ) status nrefs + List.fold_left + (fun status nref -> + let references = NCicLibrary.aliases_of nref in + let new_env = + List.map + (fun u -> + let name = NCicPp.r2s true u in + DisambiguateTypes.Id name, + LexiconAst.Ident_alias (name,NReference.string_of_reference u) + ) references + in + LexiconEngine.set_proof_aliases status new_env + ) status module OrderedId = struct diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli index c645bfdbe..acdf7fd66 100644 --- a/matita/components/lexicon/lexiconSync.mli +++ b/matita/components/lexicon/lexiconSync.mli @@ -24,8 +24,7 @@ *) val add_aliases_for_objs: - #LexiconEngine.status as 'status -> - [`Old of UriManager.uri list | `New of NUri.uri list]-> 'status + #LexiconEngine.status as 'status -> NUri.uri list -> 'status val time_travel: present:#LexiconEngine.status -> past:#LexiconEngine.status -> unit diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 1f92b5868..6f58bb54e 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -32,7 +32,7 @@ let debug_prerr = if debug then prerr_endline else ignore module HGT = Http_getter_types;; module HG = Http_getter;; -module UM = UriManager;; +(*module UM = UriManager;;*) let decompile = ref (fun ~baseuri -> assert false);; let set_decompile_cb f = decompile := f;; @@ -231,10 +231,10 @@ let clean_baseuris ?(verbose=true) buris = List.iter debug_prerr buris; let l = close_db cache_of_processed_baseuri [] buris in let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in - let l = List.map UriManager.uri_of_string l in + let l = List.map NUri.uri_of_string l in debug_prerr "clean_baseuri will remove:"; if debug then - List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; + List.iter (fun u -> debug_prerr (NUri.string_of_uri u)) l; List.iter (fun baseuri -> !decompile ~baseuri; @@ -247,4 +247,4 @@ let clean_baseuris ?(verbose=true) buris = HExtlib.rmdir_descend (Filename.chop_extension lexiconfile) with Http_getter_types.Key_not_found _ -> ()) (HExtlib.list_uniq (List.fast_sort Pervasives.compare - (List.map (UriManager.buri_of_uri) l @ buris))) + (List.map NUri.baseuri_of_uri l @ buris))) diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index dbd6523cf..5d91cee28 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -589,7 +589,7 @@ in let res = match kind with | NCic.Fixpoint (is_rec, ifl, _) -> - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Joint { K.joint_id = gen_id joint_prefix seed; K.joint_kind = @@ -599,7 +599,7 @@ in K.joint_defs = List.map (build_fixpoint is_rec seed) ifl }) | NCic.Inductive (is_ind, lno, itl, _) -> - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Joint { K.joint_id = gen_id joint_prefix seed; K.joint_kind = @@ -609,12 +609,12 @@ in | NCic.Constant (_,_,Some bo,ty,_) -> let ty = nast_of_cic ~context:[] ty in let bo = nast_of_cic ~context:[] bo in - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Def (K.Const,ty, build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty)) | NCic.Constant (_,_,None,ty,_) -> let ty = nast_of_cic ~context:[] ty in - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Decl (K.Const, (*CSC: ??? get_id ty here used to be the id of the axiom! *) build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) diff --git a/matita/components/ng_cic_content/ncic2astMatcher.ml b/matita/components/ng_cic_content/ncic2astMatcher.ml index 5acb8eb13..f6617451d 100644 --- a/matita/components/ng_cic_content/ncic2astMatcher.ml +++ b/matita/components/ng_cic_content/ncic2astMatcher.ml @@ -28,9 +28,6 @@ module Ast = NotationPt module Util = NotationUtil -let reference_of_oxuri = ref (fun _ -> assert false);; -let set_reference_of_oxuri f = reference_of_oxuri := f;; - module Matcher32 = struct module Pattern32 = @@ -50,7 +47,6 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), [] | Ast.NRefPattern nref -> NRef nref, [] | Ast.ImplicitPattern | Ast.VarPattern _ -> Blob, [] @@ -71,7 +67,6 @@ struct let classify = function | Ast.ImplicitPattern | Ast.VarPattern _ -> PatternMatcher.Variable - | Ast.UriPattern _ | Ast.NRefPattern _ | Ast.ApplPattern _ -> PatternMatcher.Constructor end diff --git a/matita/components/ng_cic_content/ncic2astMatcher.mli b/matita/components/ng_cic_content/ncic2astMatcher.mli index 1feae63b0..5d1e2c571 100644 --- a/matita/components/ng_cic_content/ncic2astMatcher.mli +++ b/matita/components/ng_cic_content/ncic2astMatcher.mli @@ -23,8 +23,6 @@ * http://helm.cs.unibo.it/ *) -val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit - module Matcher32: sig (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 071f1e00e..94643b3b0 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -42,7 +42,7 @@ let nlookup_num_by_dsc dsc = List.find (has_description dsc) !nnum_choices with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc))) -let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl_pattern)= +let mk_choice ~mk_appl ~mk_implicit ~term_of_nref (dsc, args, appl_pattern)= dsc, `Sym_interp (fun cic_args -> @@ -66,16 +66,16 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl in let combined = Interpretations.instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern + ~mk_appl ~mk_implicit ~term_of_nref env' appl_pattern in match rest with [] -> combined | _::_ -> mk_appl (combined::rest)) -let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc = +let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_nref symbol dsc = let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in try - mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref + mk_choice ~mk_appl ~mk_implicit ~term_of_nref (List.find (fun (dsc', _, _) -> dsc = dsc') interpretations) with Interpretations.Interpretation_not_found | Not_found -> raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc))) diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli index cdb7004a6..1d98fa3a6 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.mli +++ b/matita/components/ng_disambiguation/disambiguateChoices.mli @@ -45,14 +45,12 @@ val nlookup_num_by_dsc: string -> NCic.term codomain_item val lookup_symbol_by_dsc: mk_appl: ('term list -> 'term) -> mk_implicit: (bool -> 'term) -> - term_of_uri: (UriManager.uri -> 'term) -> term_of_nref: (NReference.reference -> 'term) -> string -> string -> 'term codomain_item val mk_choice: mk_appl: ('term list -> 'term) -> mk_implicit: (bool -> 'term) -> - term_of_uri: (UriManager.uri -> 'term) -> term_of_nref: (NReference.reference -> 'term) -> string * NotationPt.argument_pattern list * NotationPt.cic_appl_pattern -> diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 8d0935abc..cdb90ea02 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -14,7 +14,6 @@ open Printf open DisambiguateTypes -open UriManager module Ast = NotationPt module NRef = NReference @@ -22,9 +21,6 @@ module NRef = NReference let debug_print s = prerr_endline (Lazy.force s);; let debug_print _ = ();; -let reference_of_oxuri = ref (fun _ -> assert false);; -let set_reference_of_oxuri f = reference_of_oxuri := f;; - let cic_name_of_name = function | Ast.Ident (n, None) -> n | _ -> assert false @@ -328,7 +324,7 @@ let interpretate_term_and_interpretate_term_option | NotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri)) + NCic.Const (NReference.reference_of_string uri) with NRef.IllFormedReference _ -> NotationPt.fail loc "Ill formed reference") | NotationPt.NRef nref -> NCic.Const nref diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index 25ac95ff4..b02ce3cc8 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -11,8 +11,6 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit - val disambiguate_term : context:NCic.context -> metasenv:NCic.metasenv -> diff --git a/matita/components/urimanager/.depend b/matita/components/urimanager/.depend deleted file mode 100644 index 9cac9aa78..000000000 --- a/matita/components/urimanager/.depend +++ /dev/null @@ -1,3 +0,0 @@ -uriManager.cmi: -uriManager.cmo: uriManager.cmi -uriManager.cmx: uriManager.cmi diff --git a/matita/components/urimanager/.depend.opt b/matita/components/urimanager/.depend.opt deleted file mode 100644 index 9cac9aa78..000000000 --- a/matita/components/urimanager/.depend.opt +++ /dev/null @@ -1,3 +0,0 @@ -uriManager.cmi: -uriManager.cmo: uriManager.cmi -uriManager.cmx: uriManager.cmi diff --git a/matita/components/urimanager/Makefile b/matita/components/urimanager/Makefile deleted file mode 100644 index 592c0854e..000000000 --- a/matita/components/urimanager/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -PACKAGE = urimanager -PREDICATES = - -INTERFACE_FILES = uriManager.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/urimanager/uriManager.ml b/matita/components/urimanager/uriManager.ml deleted file mode 100644 index 2d099a4e9..000000000 --- a/matita/components/urimanager/uriManager.ml +++ /dev/null @@ -1,264 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* $Id$ *) - -(* - * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) - * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) - * "cic:/a/b/c.ind#xpointer(1/1/1)" => ("cic:/a/b/c.con#xpointer(1/1/1)", id) - *) - -let fresh_id = - let id = ref 0 in - function () -> - incr id; - !id - -(* (uriwithxpointer, uniqueid) - * where uniqueid is used to build a set of uri *) -type uri = string * int;; - -let eq uri1 uri2 = - uri1 == uri2 -;; - -let string_of_uri (uri,_) = - uri - -let name_of_uri (uri, _) = - let xpointer_offset = - try String.rindex uri '#' with Not_found -> String.length uri - 1 - in - let index1 = String.rindex_from uri xpointer_offset '/' + 1 in - let index2 = String.rindex uri '.' in - String.sub uri index1 (index2 - index1) - -let nameext_of_uri (uri, _) = - let xpointer_offset, mah = - try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1 - in - let index1 = String.rindex_from uri xpointer_offset '/' + 1 in - String.sub uri index1 (xpointer_offset - index1 + mah) - -let buri_of_uri (uri,_) = - let xpointer_offset = - try String.rindex uri '#' with Not_found -> String.length uri - 1 - in - let index = String.rindex_from uri xpointer_offset '/' in - String.sub uri 0 index - -module OrderedStrings = - struct - type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 - end -;; - -module MapStringsToUri = Map.Make(OrderedStrings);; - -(* Invariant: the map is the identity function, - * i.e. - * let str' = (MapStringsToUri.find str !set_of_uri) in - * str' == (MapStringsToUri.find str' !set_of_uri) - *) -let set_of_uri = ref MapStringsToUri.empty;; - -exception IllFormedUri of string;; - -let _dottypes = ".types" -let _types = "types",5 -let _dotuniv = ".univ" -let _univ = "univ",4 -let _dotann = ".ann" -let _ann = "ann",3 -let _var = "var",3 -let _dotbody = ".body" -let _con = "con",3 -let _ind = "ind",3 -let _xpointer = "#xpointer(1/" -let _con3 = "con" -let _var3 = "var" -let _ind3 = "ind" -let _ann3 = "ann" -let _univ4 = "univ" -let _types5 = "types" -let _xpointer8 = "xpointer" -let _cic5 = "cic:/" - -let is_malformed suri = - try - if String.sub suri 0 5 <> _cic5 then true - else - let len = String.length suri - 5 in - let last5 = String.sub suri len 5 in - let last4 = String.sub last5 1 4 in - let last3 = String.sub last5 2 3 in - if last3 = _con3 || last3 = _var3 || last3 = _ind3 || - last3 = _ann3 || last5 = _types5 || last5 = _dotbody || - last4 = _univ4 then - false - else - try - let index = String.rindex suri '#' + 1 in - let xptr = String.sub suri index 8 in - if xptr = _xpointer8 then - false - else - true - with Not_found -> true - with Invalid_argument _ -> true - -(* hash conses an uri *) -let uri_of_string suri = - try - MapStringsToUri.find suri !set_of_uri - with Not_found -> - if is_malformed suri then - raise (IllFormedUri suri) - else - let new_uri = suri, fresh_id () in - set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; - new_uri - - -let strip_xpointer ((uri,_) as olduri) = - try - let index = String.rindex uri '#' in - let no_xpointer = String.sub uri 0 index in - uri_of_string no_xpointer - with - Not_found -> olduri - -let clear_suffix uri ?(pat2="",0) pat1 = - try - let index = String.rindex uri '.' in - let index' = index + 1 in - let suffix = String.sub uri index' (String.length uri - index') in - if fst pat1 = suffix || fst pat2 = suffix then - String.sub uri 0 index - else - uri - with - Not_found -> assert false - -let has_suffix uri (pat,n) = - try - let suffix = String.sub uri (String.length uri - n) n in - pat = suffix - with - Not_found -> assert false - - -let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann) - -let annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann) - -let uri_is_annuri (uri, _) = has_suffix uri _ann - -let uri_is_var (uri, _) = has_suffix uri _var - -let uri_is_con (uri, _) = has_suffix uri _con - -let uri_is_ind (uri, _) = has_suffix uri _ind - -let bodyuri_of_uri (uri, _) = - if has_suffix uri _con then - Some (uri_of_string (uri ^ _dotbody)) - else - None -;; - -let ind_uri_split ((s, _) as uri) = - let noxp = strip_xpointer uri in - try - (let arg_index = String.rindex s '(' in - try - (let ty_index = String.index_from s arg_index '/' in - try - (let k_index = String.index_from s (ty_index+1) '/' in - let tyno = int_of_string (String.sub s (ty_index + 1) (k_index - ty_index - 1)) in - let kno = int_of_string (String.sub s (k_index + 1) (String.length s - k_index - 2)) in - noxp, Some tyno, Some kno) - with Not_found -> - let tyno = int_of_string (String.sub s (ty_index + 1) (String.length s - ty_index - 2)) in - noxp, Some tyno, None) - with Not_found -> noxp, None, None - ) - with Not_found -> noxp, None, None -;; - -(* these are bugged! - * we should remove _types, _univ, _ann all toghether *) -let innertypesuri_of_uri (uri, _) = - uri_of_string ((clear_suffix uri _types) ^ _dottypes) -;; -let univgraphuri_of_uri (uri,_) = - uri_of_string ((clear_suffix uri _univ) ^ _dotuniv) -;; - - -let uri_of_uriref (uri, _) typeno consno = - let typeno = typeno + 1 in - let suri = - match consno with - | None -> Printf.sprintf "%s%s%d)" uri _xpointer typeno - | Some n -> Printf.sprintf "%s%s%d/%d)" uri _xpointer typeno n - in - uri_of_string suri - -let compare (_,id1) (_,id2) = id1 - id2 - -module OrderedUri = -struct - type t = uri - let compare = compare (* the one above, not Pervasives.compare *) -end - -module UriSet = Set.Make (OrderedUri) - -(* -module OrderedUriPair = -struct - type t = uri * uri - let compare (u11, u12) (u21, u22) = - match compare u11 u21 with - | 0 -> compare u12 u22 - | x -> x -end - -module UriPairSet = Set.Make (OrderedUriPair) -*) - -module HashedUri = -struct - type t = uri - let equal = eq - let hash = snd -end - -module UriHashtbl = Hashtbl.Make (HashedUri) - - diff --git a/matita/components/urimanager/uriManager.mli b/matita/components/urimanager/uriManager.mli deleted file mode 100644 index 99e65ab88..000000000 --- a/matita/components/urimanager/uriManager.mli +++ /dev/null @@ -1,75 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception IllFormedUri of string;; - -type uri - -val eq : uri -> uri -> bool -val compare : uri -> uri -> int - -val uri_of_string : string -> uri - -val string_of_uri : uri -> string (* complete uri *) -val name_of_uri : uri -> string (* name only (without extension)*) -val nameext_of_uri : uri -> string (* name only (with extension)*) -val buri_of_uri : uri -> string (* base uri only, without trailing '/' *) - -(* given an uri, returns the uri of the corresponding cic file, *) -(* i.e. removes the [.types][.ann] suffix *) -val cicuri_of_uri : uri -> uri - -val strip_xpointer: uri -> uri (* remove trailing #xpointer..., if any *) - -(* given an uri, returns the uri of the corresponding annotation file, *) -(* i.e. adds the .ann suffix if not already present *) -val annuri_of_uri : uri -> uri - -val uri_is_annuri : uri -> bool -val uri_is_var : uri -> bool -val uri_is_con : uri -> bool -val uri_is_ind : uri -> bool - -(* given an uri of a constant, it gives back the uri of its body *) -(* it gives back None if the uri refers to a Variable or MutualInductiveType *) -val bodyuri_of_uri : uri -> uri option - -val ind_uri_split : uri -> uri * int option * int option - -(* given an uri, it gives back the uri of its inner types *) -val innertypesuri_of_uri : uri -> uri -(* given an uri, it gives back the uri of its univgraph *) -val univgraphuri_of_uri : uri -> uri - -(* builder for MutInd and MutConstruct URIs - * [uri] -> [typeno] -> [consno option] - *) -val uri_of_uriref : uri -> int -> int option -> uri - -module UriSet: Set.S with type elt = uri -(*module UriPairSet: Set.S with type elt = uri * uri*) - -module UriHashtbl : Hashtbl.S with type key = uri - diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade index 0934b8102..3b87423d0 100644 --- a/matita/matita/matita.glade +++ b/matita/matita/matita.glade @@ -86,13 +86,6 @@ True - - - True - Universes - True - - True diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 99fa10acb..cefb46e29 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -82,14 +82,8 @@ let _ = sequents_viewer#load_logo; cic_math_view#set_href_callback (Some (fun uri -> - let uri = - try - `Uri (UriManager.uri_of_string uri) - with - UriManager.IllFormedUri _ -> - `NRef (NReference.reference_of_string uri) - in - (MatitaMathView.cicBrowser ())#load uri)); + let uri = `NRef (NReference.reference_of_string uri) in + (MatitaMathView.cicBrowser ())#load uri)); let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer grafite_status = sequents_viewer#reset; diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index 99e6ec944..f6bd9b90c 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -121,7 +121,6 @@ let rec to_string = | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err - | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri | Unix.Unix_error (code, api, param) -> let err = Unix.error_message code in None, "Unix Error (" ^ api ^ "): " ^ err diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index a0d731377..6f4e09bbc 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -1399,11 +1399,10 @@ let interactive_uri_choice ~id uris = let gui = instance () in - let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in if (selection_mode <> `SINGLE) && (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") then - Lazy.force nonvars_uris + uris else begin let dialog = gui#newUriDialog () in if hide_uri_entry then @@ -1429,7 +1428,7 @@ let interactive_uri_choice | _ -> ())); dialog#uriChoiceDialog#set_title title; dialog#uriChoiceLabel#set_text msg; - List.iter model#easy_append (List.map UriManager.string_of_uri uris); + List.iter model#easy_append (List.map NReference.string_of_reference uris); dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; let return v = choices := v; @@ -1438,20 +1437,20 @@ let interactive_uri_choice in ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); connect_button dialog#uriChoiceConstantsButton (fun _ -> - return (Some (Lazy.force nonvars_uris))); + return (Some uris)); if ok_action = `AUTO then connect_button dialog#uriChoiceAutoButton (fun _ -> Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some (Lazy.force nonvars_uris))) + return (Some uris)) else connect_button dialog#uriChoiceAutoButton (fun _ -> match model#easy_selection () with | [] -> () - | uris -> return (Some (List.map UriManager.uri_of_string uris))); + | uris -> return (Some (List.map NReference.reference_of_string uris))); connect_button dialog#uriChoiceSelectedButton (fun _ -> match model#easy_selection () with | [] -> () - | uris -> return (Some (List.map UriManager.uri_of_string uris))); + | uris -> return (Some (List.map NReference.reference_of_string uris))); connect_button dialog#uriChoiceAbortButton (fun _ -> return None); dialog#uriChoiceDialog#show (); GtkThread.main (); diff --git a/matita/matita/matitaGui.mli b/matita/matita/matitaGui.mli index 796c33fef..d3c09a2f4 100644 --- a/matita/matita/matitaGui.mli +++ b/matita/matita/matitaGui.mli @@ -43,7 +43,7 @@ val interactive_uri_choice: ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string -> ?ok_action:[`AUTO|`SELECT] -> ?copy_cb:(string -> unit) -> unit -> - id:'a -> UriManager.uri list -> UriManager.uri list + id:'a -> NReference.reference list -> NReference.reference list (** @raise MatitaTypes.Cancel *) val interactive_interp_choice: diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 480bf1210..f418abe6f 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -995,7 +995,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) object (self) inherit scriptAccessor - val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con"; + val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec"; val dep_contextual_menu = GMenu.menu () @@ -1021,20 +1021,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> - let uri = - try - `Uri (UriManager.uri_of_string uri) - with - UriManager.IllFormedUri _ -> - `NRef (NReference.reference_of_string uri) - in + let uri = `NRef (NReference.reference_of_string uri) in self#load uri))); gviz#connect_href (fun button_ev attrs -> let time = GdkEvent.Button.time button_ev in let uri = List.assoc "href" attrs in - gviz_uri <- UriManager.uri_of_string uri; + gviz_uri <- NReference.reference_of_string uri; match GdkEvent.Button.button button_ev with - | button when button = left_button -> self#load (`Uri gviz_uri) + | button when button = left_button -> self#load (`NRef gviz_uri) | button when button = right_button -> dep_contextual_menu#popup ~button ~time | _ -> ()); @@ -1050,10 +1044,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) win#hBugsTutorsMenuItem#misc#hide (); connect_menu_item win#browserUrlMenuItem (fun () -> win#browserUri#misc#grab_focus ()); - connect_menu_item win#univMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Univs uri) - | None -> ()); self#_load (`About `Blank); toplevel#show () @@ -1063,7 +1053,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** @return None if no object uri can be built from the current entry *) method private currentCicUri = match current_entry with - | `Uri uri -> Some uri + | `NRef uri -> Some uri | _ -> None val model = @@ -1147,9 +1137,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors - | `Uri uri -> assert false (* MATITA 1.0 *) - | `NRef nref -> self#_loadNReference nref - | `Univs uri -> assert false (* MATITA 1.0 *)); + | `NRef nref -> self#_loadNReference nref); self#setEntry entry end) @@ -1174,7 +1162,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; (match center_on with | None -> () - | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri)); + | Some uri -> gviz#center_on_href (NReference.string_of_reference uri)); HExtlib.safe_remove tmpfile else MatitaGtkMisc.report_error ~title:"graphviz error" @@ -1314,7 +1302,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let entry = match txt with | txt when is_uri txt -> - `Uri (UriManager.uri_of_string ((*fix_uri*) txt)) + `NRef (NReference.reference_of_string ((*fix_uri*) txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) | txt -> (try diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 3ab92575c..6221e4901 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -67,7 +67,7 @@ let first_line s = type guistuff = { mathviewer:MatitaTypes.mathViewer; - urichooser: UriManager.uri list -> UriManager.uri list; + urichooser: NReference.reference list -> NReference.reference list; ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 85c4e767a..50bc17eda 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -86,7 +86,7 @@ end val script: source_view:GSourceView2.source_view -> mathviewer: MatitaTypes.mathViewer-> - urichooser: (UriManager.uri list -> UriManager.uri list) -> + urichooser: (NReference.reference list -> NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> set_star: (bool -> unit) -> diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index 854bbca16..1f7c50729 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -47,9 +47,7 @@ type mathViewer_entry = | `Check of string (* term *) | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string (* "directory" in cic uris namespace *) - | `Uri of UriManager.uri (* cic object uri *) | `NRef of NReference.reference (* cic object uri *) - | `Univs of UriManager.uri ] let string_of_entry = function @@ -64,9 +62,7 @@ let string_of_entry = function | `Check _ -> "check:" | `NCic (_, _, _, _) -> "nterm:" | `Dir uri -> uri - | `Uri uri -> UriManager.string_of_uri uri | `NRef nref -> NReference.string_of_reference nref - | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri let entry_of_string = function | "about:blank" -> `About `Blank @@ -87,7 +83,7 @@ class type mathViewer = *) method show_entry: ?reuse:bool -> mathViewer_entry -> unit method show_uri_list: - ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit + ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit method screenshot: GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> NCic.substitution -> string -> unit diff --git a/matita/matita/matitaTypes.mli b/matita/matita/matitaTypes.mli index 9cb7ac984..3509f0ee7 100644 --- a/matita/matita/matitaTypes.mli +++ b/matita/matita/matitaTypes.mli @@ -33,9 +33,7 @@ type mathViewer_entry = | `Check of string | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string - | `Uri of UriManager.uri | `NRef of NReference.reference - | `Univs of UriManager.uri ] val string_of_entry : mathViewer_entry -> string @@ -45,7 +43,7 @@ class type mathViewer = object method show_entry : ?reuse:bool -> mathViewer_entry -> unit method show_uri_list : - ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit + ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit method screenshot: GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> NCic.substitution -> string -> unit diff --git a/matita/matita/matitaclean.ml b/matita/matita/matitaclean.ml index f0f45b126..d04e9fba9 100644 --- a/matita/matita/matitaclean.ml +++ b/matita/matita/matitaclean.ml @@ -27,7 +27,6 @@ open Printf -module UM = UriManager module TA = GrafiteAst let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ] @@ -107,14 +106,15 @@ let main () = List.fold_left (fun uris_to_remove suri -> let uri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with UM.IllFormedUri _ -> + (*MATITA 1.0, CSC: verify that suri is a reasonable uri *) + (*try*) + NUri.baseuri_of_uri (NUri.uri_of_string suri) + (*with UM.IllFormedUri _ -> let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in if Librarian.is_uri u then u else begin HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); exit 1 - end + end *) in uri::uris_to_remove) [] files in diff --git a/matita/matita/matitadep.ml b/matita/matita/matitadep.ml index 73ce0cd81..315678307 100644 --- a/matita/matita/matitadep.ml +++ b/matita/matita/matitadep.ml @@ -28,7 +28,6 @@ module S = Set.Make (String) module GA = GrafiteAst -module U = UriManager module HR = Helm_registry let print_times msg = @@ -104,7 +103,7 @@ let main () = HLog.error ("possibly incorrect verbatim URIs in the .ma file."); None in - let buri alias = U.buri_of_uri (U.uri_of_string alias) in + let buri alias = NUri.baseuri_of_uri (NUri.uri_of_string alias) in let resolve alias current_buri = let buri = buri alias in if buri <> current_buri then Some buri else None @@ -190,7 +189,7 @@ let main () = List.iter (function | DependenciesParser.UriDep uri -> - let uri = UriManager.string_of_uri uri in + let uri = NUri.string_of_uri uri in handle_uri uri | DependenciesParser.InlineDep path -> if Librarian.is_uri path -- 2.39.2