*)
open Printf
-
open MatitaTypes
+let debug = true
+let debug_print = if debug then prerr_endline else ignore
+
(** raised when one of the script margins (top or bottom) is reached *)
exception Margin
let module UM = UriManager in
DTE.fold (
fun k ((v,_) as value) acc ->
- let v = UM.strip_xpointer (UM.uri_of_string v) in
- if List.exists (fun (s,_) -> s = v) new_status.objects then
+ let b =
+ try
+ let v = UM.strip_xpointer (UM.uri_of_string v) in
+ List.exists (fun (s,_) -> s = v) new_status.objects
+ with UM.IllFormedUri _ -> false
+ in
+ if b then
acc
else
DTE.add k value acc
let term = disambiguate term status in
let uri =
match term with
- | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
+ | Cic.MutInd (uri,n,_) -> UriManager.uri_of_string (UriManager.string_of_uriref (uri,[n]))
| _ -> failwith "Not a MutInd"
in
let l = MQ.elim ~dbd uri in
(TA.Executable (loc,
(TA.Tactical (loc,
TA.Tactic (loc,
- TA.Apply (loc, CicAst.Uri (uri,None)))))))
+ TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))))
in
let new_status = MatitaEngine.eval_ast status ast in
let extra_text =
MatitaLog.error
"The result of the urichooser should be only 1 uri, not:\n";
List.iter (
- fun u -> MatitaLog.error (u ^ "\n")
+ fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
) selected;
assert false)
| TA.Check (_,term) ->