added owner support to the disambiguator (now locate finds only objects

of the current owner).

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index aafbeb7777d85689fab91712b412761119476ed2..b36ae5b119ecba762c529f79baeb52181f987fb8 100644 (file)
--- 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 dbd id =
-      let uris = MetadataQuery.locate ~dbd id in
+    let choices_of_id ?owner dbd id =
+      let uris = MetadataQuery.locate ?owner ~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)  ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~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 dbd id in
+                let choices = choices_of_id ?owner 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 b0fe0fcd3e7dfa11f4a874d998971b198f2f14d2..b240ea035cac68adb1a9874a8878135e999d1e37 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -37,6 +37,7 @@ 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 f65318896ae7bd9c57718021fa4df7edc978acb4..4e6b31b537ce880232b591cccc3f9197bd8726dc 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -46,11 +46,23 @@ let nonvar s =
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
-      MetadataTypes.name_tbl sql_pat
+    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 0d32e4835c39ec8442b75bf88e826aa08e7778bd..4ae870a4f4e484c2e6eb19665809f32ae514ddfc 100644 (file)
--- 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 -> string -> string list
+  ?vars:bool -> ?owner:string -> string -> string list
 
 val hint:
   dbd:Mysql.dbd ->