X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FbatchParser.mli;h=b63845aa871281c5b1c6e2309d310f2a258f52b2;hb=edb6ab182b915ebc8b2810574b0a87bdab39d051;hp=7d8f4bcd709651865faf55b5331fb92f946c2c9f;hpb=c35a3f47e0468a6076a3afdd6f2ff5c5fe528784;p=helm.git

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index 7d8f4bcd7..b63845aa8 100644
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -25,12 +25,22 @@
 
 exception Failure of string
 
+  (** uri_pred which rejects ll .var URIs *)
+val constants_only: (string -> bool)
+
+  (** @param variables enabled
+   * @param variables prefix
+   * @return uri predicate suitable for functions below *)
+val uri_pred_of_conf: bool -> 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: ?uri_pred:(string -> bool) -> string -> Cic.metasenv * Cic.term
 
   (** as above, but instead of returning the parsed cic term, pretty prints it
    * (ignoring returned metasenv)
    *)
-val parse_pp: string -> string
+val parse_pp: ?uri_pred:(string -> bool) -> string -> string