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 = "")
~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
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)
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 =
(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
(* 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 =
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
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 *)