*)
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
DisambiguateTypes.Environment.empty
| _ -> MatitaSync.alias_diff ~from:status new_status
in
+ (* we remove the defined object since we consider them "automathic aliases" *)
+ let new_aliases =
+ let module DTE = DisambiguateTypes.Environment in
+ let module UM = UriManager in
+ DTE.fold (
+ fun k ((v,_) as value) acc ->
+ 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
+ ) new_aliases DTE.empty
+ in
let new_text =
if DisambiguateTypes.Environment.is_empty new_aliases then
parsed_text
"\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