incomplete proof completed

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 58043bbd3d5acb44ab3af00adb206135c8f12f24..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
 
@@ -91,8 +93,13 @@ let eval_with_engine status user_goal parsed_text st =
     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
@@ -196,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