aded confirmation dialog for baseuri redefinement

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 9ca48d9cab897d2dc4f996f6a0c3d48a56f4ba2d..4f7027d61c83170577041400eafce92a5ea0a40e 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -251,21 +251,34 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser
 
                                 
 let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser
-user_goal parsed_text script ex =
+ask_confirmation user_goal parsed_text script ex =
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
   let module MD = MatitaDisambiguator in
   let parsed_text_length = String.length parsed_text in
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _) ->
-      eval_with_engine status user_goal parsed_text
-       (TA.Executable (loc, ex))
+      (match MatitacleanLib.baseuri_of_baseuri_decl (TA.Executable (loc,ex))with
+      | None -> ()
+      | Some u -> 
+          if not (MatitacleanLib.is_empty u) then
+            match 
+              ask_confirmation 
+                ~title:"Baseuri redefinition" 
+                ~message:(
+                  "Baseuri " ^ u ^ " already exists.\n" ^
+                  "Do you want to redefine the corresponding "^
+                  "part of the library?")
+            with
+            | `YES -> MatitacleanLib.clean_baseuris [u]
+            | `NO -> ()
+            | `CANCEL -> raise MatitaTypes.Cancel);
+      eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex))
   | TA.Macro (_,mac) ->
       eval_macro status mathviewer urichooser parsed_text script mac
 
-let rec eval_statement status (mathviewer:MatitaTypes.mathViewer)
- urichooser user_goal script s
-=
+let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser
+ask_confirmation user_goal script s =
   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
   let st = CicTextualParser2.parse_statement (Stream.of_string s) in
   let text_of_loc loc =
@@ -279,7 +292,8 @@ let rec eval_statement status (mathviewer:MatitaTypes.mathViewer)
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
       let s,len = 
-        eval_statement status mathviewer urichooser user_goal script s 
+        eval_statement status 
+          mathviewer urichooser ask_confirmation user_goal script s 
       in
       (match s with
       | (status, text) :: tl ->
@@ -287,8 +301,9 @@ let rec eval_statement status (mathviewer:MatitaTypes.mathViewer)
       | [] -> [], 0)
   | TacticAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
-       eval_executable status mathviewer urichooser user_goal
-        parsed_text script ex
+      eval_executable 
+        status mathviewer urichooser ask_confirmation 
+          user_goal parsed_text script ex
   
 let fresh_script_id =
   let i = ref 0 in
@@ -297,6 +312,7 @@ let fresh_script_id =
 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
+              ~ask_confirmation
               ~urichooser () =
 object (self)
   val mutable filename = None
@@ -341,7 +357,9 @@ object (self)
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
     let (entries, parsed_len) = 
-      eval_statement self#status mathviewer urichooser userGoal self s in
+      eval_statement self#status 
+        mathviewer urichooser ask_confirmation userGoal self s 
+    in
     let (new_statuses, new_statements) = List.split entries in
 (*
 prerr_endline "evalStatement returned";
@@ -499,8 +517,11 @@ end
 
 let _script = ref None
 
-let script ~buffer ~init ~mathviewer ~urichooser ~set_star () =
-  let s = new script ~buffer ~init ~mathviewer ~urichooser ~set_star () in
+let script ~buffer ~init ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
+=
+  let s = new script 
+    ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~set_star () 
+  in
   _script := Some s;
   s