*)
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
"\n" ^ TAPp.pp_statement ast
in
[ new_status , extra_text ], parsed_text_length
- | _ -> assert false)
+ | _ ->
+ MatitaLog.error
+ "The result of the urichooser should be only 1 uri, not:\n";
+ List.iter (
+ fun u -> MatitaLog.error (u ^ "\n")
+ ) selected;
+ assert false)
| TA.Check (_,term) ->
let metasenv = MatitaMisc.get_proof_metasenv status in
let context = MatitaMisc.get_proof_context status in