New functions UriManager.uri_is_var, UriManager.uri_is_con.

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8915f7681270ad43bdb94a009047820ac657f10d..34cf20afa4eb42bb0232ee13cd680e9faf024137 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -401,12 +401,6 @@ let instance = singleton gui
 
 let non p x = not (p x)
 
-let is_var_uri s =
-  let s = UriManager.string_of_uri s in
-  try
-    String.sub s (String.length s - 4) 4 = ".var"
-  with Invalid_argument _ -> false
-
 (* this is a shit and should be changed :-{ *)
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
@@ -416,7 +410,7 @@ let interactive_uri_choice
   ~id uris
 =
   let gui = instance () in
-  let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
+  let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
   if (selection_mode <> `SINGLE) &&
     (Helm_registry.get_bool "matita.auto_disambiguation")
   then

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 81055e68178099bd41523c9e870b07d83be84194..149a9bc2e1f2b028c7c30dfb0ed0d2d30984bc0b 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -141,9 +141,9 @@ let slash_RE = Str.regexp "/"
 let term_of_uri uri =
   let s = UriManager.string_of_uri uri in
   try
-    (if String.sub s (String.length s - 4) 4 = ".con" then
+    (if UriManager.uri_is_con uri then
       Cic.Const (uri, [])
-    else if String.sub s (String.length s - 4) 4 = ".var" then
+    else if UriManager.uri_is_var uri then
       Cic.Var (uri, [])
     else if not (Str.string_match xpointer_RE s 0) then
       raise (UriManager.IllFormedUri s)

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index 6ebdf8e1fac2cd0c94c5ae35b5da5060bdcec88e..defc33f6cc63e6eef9b18b7c40332f0008214775 100644 (file)
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -24,31 +24,6 @@ let indconuri_of_uri uri =
     int_of_string
       (String.sub uri index_con (String.length uri - index_con)))
 
-(*  (* NO LONGER USED, see CicUtil.term_of_uri *)
-let term_of_uri ?(subst = []) uri =
-  let s = UriManager.string_of_uri uri in
-  try
-  (* Constant *)
-  let len = String.length s in
-  let sub = String.sub s (len -4) 4 in
-  if sub = ".con" then
-    const ~subst uri
-  else if sub = ".var" then
-    var ~subst uri
-  else
-    (try
-      (* Inductive Type *)
-      let (uri, typeno) = indtyuri_of_uri s in
-      mutind ~subst uri typeno
-     with
-      | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
-          (* Constructor of an Inductive Type *)
-          let (uri, typeno, consno) = indconuri_of_uri s in
-          mutconstruct ~subst uri typeno consno)
- with
- | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)
-*)
-
 (** {2 Helm's objects shorthands} *)
 
 module Logic =

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index c1dd20ecc83badb808fb8e303b7feec3d701bbbf..ed4418dd2e5ef53eda901bf3d06a89ce1ea526c2 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -43,11 +43,7 @@ let sqlpat_of_shellglob =
           (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
             shellglob)))
 
-let nonvar s =
-  let s = UriManager.string_of_uri s in
-  let len = String.length s in
-  let suffix = String.sub s (len-4) 4 in
-  not (suffix  = ".var")
+let nonvar uri = not (UriManager.uri_is_var uri)
 
 let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 2d1b0dcfd14833a5cebde6d5598b9046bfe7c6b6..de356a3d1f52860237a9582bb57b0ddc991e271f 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -125,11 +125,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   (* List.iter 
     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
   (* delete all .var uris *)
-  let isvar (_,s) =
-    let len = String.length s in
-    let suffix = String.sub s (len-4) 4 in
-      not (suffix  = ".var") in
-  let uris = List.filter isvar uris in 
+  let uris = List.filter UriManager.is_var uris in 
   (* delete all not "cic:/Coq" uris *)
   (*
   let uris =

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 4c489a9fdaa6988edda7c176cf8e735f2b14b53d..f701125eda0d9c0d98ccf74f16c06eb62a63d116 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -122,21 +122,15 @@ let _dotbody = ".body"
 let _con = "con"
 let _xpointer = "#xpointer(1/"
  
-let cicuri_of_uri (uri, _) =
-  uri_of_string (clear_suffix uri ~pat2:_types _ann)
-;;
+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 annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann)
 
-let uri_is_annuri (uri, _) =
-  has_suffix uri _ann
-;;
+let uri_is_annuri (uri, _) = has_suffix uri _ann
 
-let uri_is_var (uri, _) =
-  has_suffix uri _var
-;;
+let uri_is_var (uri, _) = has_suffix uri _var
+
+let uri_is_con (uri, _) = has_suffix uri _con
 
 let bodyuri_of_uri (uri, _) =
   if has_suffix uri _con then

diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 27bf862b8f11ad0d9782d1adfb6776da1c39ef38..bed9db29ea43ce8f02d56e70490c75dc47b64ae4 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -48,6 +48,7 @@ val annuri_of_uri : uri -> uri
 
 val uri_is_annuri : uri -> bool
 val uri_is_var : uri -> bool
+val uri_is_con : 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 *)