X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FbatchParser.mli;h=b6410fe3bc1af096d6e6b8ae4c1c9847c9e9a989;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=ba5d5ab5801f89c08ccdad56d21c74ec009dff63;hpb=c911fe913e84cda448e2f0df20c1e023f6f8043d;p=helm.git

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index ba5d5ab58..b6410fe3b 100644
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -26,21 +26,24 @@
 exception Failure of string
 
   (** uri_pred which rejects ll .var URIs *)
-val constants_only: (string -> bool)
+val constants_only: prefix:string -> (string -> bool)
 
   (** @param variables enabled
-   * @param variables prefix
+   * @param variables prefix varsprefix
    * @return uri predicate suitable for functions below *)
-val uri_pred_of_conf: bool -> string -> (string -> bool)
+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.
    * 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 -> Cic.metasenv * Cic.term
+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: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string
+val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string list