]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/batchParser.mli
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / batchParser.mli
index 7d8f4bcd709651865faf55b5331fb92f946c2c9f..6d2900304a228708270a8268e1f947c367c13b74 100644 (file)
 
 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:
+ Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->  
+  CicUniv.universe_graph ->
+  (DisambiguatingParser.EnvironmentP3.t * 
+   Cic.metasenv * 
+   Cic.term * 
+   CicUniv.universe_graph) 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: Mysql.dbd -> ?uri_pred:(string -> bool) -> 
+  string -> CicUniv.universe_graph -> string list