From: Enrico Tassi Date: Tue, 1 Feb 2005 15:40:15 +0000 (+0000) Subject: reverder change. no more owner passed to the locate. X-Git-Tag: V_0_1_0~71 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1bfef9d9930c9a136abe0593d8da457b4e21fc3;p=helm.git reverder change. no more owner passed to the locate. --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b36ae5b11..67b6d115c 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -421,8 +421,8 @@ let domain_diff dom1 dom2 = module Make (C: Callbacks) = struct - let choices_of_id ?owner dbd id = - let uris = MetadataQuery.locate ?owner ~dbd id in + let choices_of_id dbd id = + let uris = MetadataQuery.locate ~dbd id in let uris = match uris with | [] -> @@ -452,7 +452,7 @@ module Make (C: Callbacks) = uris let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term - ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -477,7 +477,7 @@ module Make (C: Callbacks) = (try Hashtbl.find id_choices id with Not_found -> - let choices = choices_of_id ?owner dbd id in + let choices = choices_of_id dbd id in Hashtbl.add id_choices id choices; choices) | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index b240ea035..b0fe0fcd3 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -37,7 +37,6 @@ module Make (C : Callbacks) : Cic.metasenv -> CicAst.term -> ?initial_ugraph:CicUniv.universe_graph -> - ?owner:string -> aliases:environment -> (* previous interpretation status *) (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 4e6b31b53..52bd953a9 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -46,23 +46,11 @@ let nonvar s = let suffix = String.sub s (len-4) 4 in not (suffix = ".var") -let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat = +let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = let sql_pat = sqlpat_of_shellglob pat in let query = - match owner with - | None -> sprintf "SELECT source FROM %s WHERE value LIKE \"%s\"" MetadataTypes.name_tbl sql_pat - | Some owner -> - sprintf "SELECT %s.source FROM %s,%s WHERE - (%s.source LIKE CONCAT(%s.source,\"#%%\") OR - %s.source = %s.source) AND - value LIKE \"%s\" AND owner = \"%s\"" - MetadataTypes.name_tbl - MetadataTypes.name_tbl MetadataTypes.owners_tbl - MetadataTypes.name_tbl MetadataTypes.owners_tbl - MetadataTypes.name_tbl MetadataTypes.owners_tbl - sql_pat owner in let result = Mysql.exec dbd query in List.filter nonvar diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 4ae870a4f..0d32e4835 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -29,7 +29,7 @@ * is interpreted as 0 or more characters and "?" as exactly one character *) val locate: dbd:Mysql.dbd -> - ?vars:bool -> ?owner:string -> string -> string list + ?vars:bool -> string -> string list val hint: dbd:Mysql.dbd ->