exception Failure of string
+ (** uri_pred which rejects ll .var URIs *)
+val constants_only: prefix:string -> (string -> bool)
+
+ (** @param variables enabled
+ * @param variables prefix varsprefix
+ * @return uri predicate suitable for functions below *)
+val uri_pred_of_conf:
+ bool -> prefix:string -> varsprefix:string -> (string -> bool)
+
(** Parse a cic term from the given string using disambiguating parser in
- * batch mode if possible, otherwise raises Failure above *)
-val parse: string -> Cic.metasenv * Cic.term
+ * batch mode if possible, otherwise raises Failure above.
+ * uri_pred is the predicate used to select which uris are tried. Per default
+ * only constant URIs are accepted *)
+val parse:
+ MQIConn.handle -> ?uri_pred:(string -> bool) -> string ->
+ (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
(** as above, but instead of returning the parsed cic term, pretty prints it
* (ignoring returned metasenv)
*)
-val parse_pp: string -> string
+val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string list