title:string -> msg:string -> id:string -> string list -> string list
val interactive_interpretation_choice :
(string * string) list list -> int list
- val input_or_locate_uri : title:string -> UriManager.uri
+ val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri
end
;;
[] ->
[UriManager.string_of_uri
(C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
C.interactive_user_uri_choice
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
+ let term,_,metasenv'',_ = (* TASSI: FIXME what are we doning here?*)
+ CicRefine.type_of_aux' metasenv' context expr CicUniv.empty_ugraph
in
- Ok (term,metasenv'')
+ Ok (term,metasenv'') (* TASSI: whould we pass back the ugraph? *)
with
CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
Uncertain
- | _ ->
+ | CicRefine.RefineFailure _ ->
prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
Ko
in
let regexpr =
let alfa = "[a-zA-Z_-]" in
let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
+ let ident = alfa ^ "\\(" ^ alfa ^ "\\|" ^ digit ^ "\\)*" in
+ let blanks = "\\( \\|\t\\|\n\\)+" in
let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
+ let uri = "/\\(" ^ ident ^ "/\\)*" ^ nonblanks in
+ (* not very strict check *)
Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
+ ("alias" ^ blanks ^ "\\(" ^ ident ^ "\\)" ^ blanks ^ "\\(" ^ uri ^ "\\)")
in
let rec aux n =
try