...

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c8fbba9bee8a66c777ff205cb0d351aef5841ff4..26a0f2487503af6530841f54bc9b3c8cc0c35274 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -24,9 +24,11 @@
  *)
 
 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
 
@@ -85,6 +87,24 @@ let eval_with_engine status user_goal parsed_text st =
           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
@@ -183,7 +203,13 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser 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