aded confirmation dialog for baseuri redefinement

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 93441ed83fc5627e64927a7d33e7c26a54b34905..3eb0fc6a15f985c897e07144b0949c41688805d7 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -87,6 +87,10 @@ let script =
         () ~id:"boh?" uris
       with MatitaTypes.Cancel -> [])
     ~set_star:gui#setStar
+    ~ask_confirmation:
+      (fun ~title ~message -> 
+          MatitaGtkMisc.ask_confirmation ~title ~message 
+          ~parent:gui#main#toplevel ())
     ()
 
   (* math viewers *)

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f913639f945e2f0c2919dfd2e77355d195f0144d..2151541a32aa179f165b51993a97138dd16fa866 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -351,7 +351,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
   let fail message = 
-    MatitaGtkMisc.report_error ~title:"Cic browser" ~message ()  
+    MatitaGtkMisc.report_error ~title:"Cic browser" ~message 
+      ~parent:toplevel ()  
   in
   let tags =
     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");

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
 

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index 677006b7195fb4be17e4ae4fd75d4e2673660f01..af1c68cc350d58c74cd5839e0f28c8895edfc116 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -69,6 +69,8 @@ val script:
   init:MatitaTypes.status -> 
   mathviewer: MatitaTypes.mathViewer-> 
   urichooser: (UriManager.uri list -> UriManager.uri list) -> 
+  ask_confirmation: 
+    (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> 
   set_star: (string -> bool -> unit) ->
   unit -> 
     script

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 76ec992beedb7eea566de178a5e73d8167a20dd8..8f8a66e098fc9378e73ace85e7c2d1a5d8e93e05 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -252,6 +252,7 @@ let remove uri =
           assert (String.sub path 0 7 = "file://");
           String.sub path 7 (String.length path - 7)
         in
+        MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
         remove_object_from_disk uri path; 
       with
         Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri);

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index 992443a357681615771315cac4710c87aadd067b..f8376416e706ebfad00242b502d4b49b5e25f5a8 100644 (file)
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -1,8 +1,16 @@
 module HGT = Http_getter_types;;
 module HG = Http_getter;;
+module HGM = Http_getter_misc;;
 module UM = UriManager;;
 module TA = TacticAst;;
 
+let baseuri_of_baseuri_decl st =
+  let module TA = TacticAst in
+  match st with
+  | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
+      Some buri
+  | _ -> None
+
 let cache_of_processed_baseuri = Hashtbl.create 1024
 
 let one_step_depend suri =
@@ -21,12 +29,17 @@ let one_step_depend suri =
         let buri = Mysql.escape buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
         Printf.sprintf 
-          "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+          "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
       in
       try 
         let rc = Mysql.exec (MatitaDb.instance ()) query in
         let l = ref [] in
-        Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l);
+        Mysql.iter rc (
+          fun row -> 
+            match row.(0), row.(1) with 
+            | Some uri, Some occ when Filename.dirname occ = buri -> 
+                l := uri :: !l
+            | _ -> ());
         let l = List.sort Pervasives.compare !l in
         MatitaMisc.list_uniq l
       with
@@ -90,10 +103,10 @@ let baseuri_of_file file =
   close_in ic;
   let uri = ref "" in
   List.iter 
-    (function
-    | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
-        uri := MatitaMisc.strip_trailing_slash buri
-    | _ -> ()) 
+    (fun stm ->
+      match baseuri_of_baseuri_decl stm with
+      | Some buri -> uri := MatitaMisc.strip_trailing_slash buri
+      | None -> ())
     stms;
   !uri
 
@@ -103,8 +116,12 @@ let rec fix uris next =
   | l -> let uris, next = close_uri_list l in fix uris next @ uris
   
 let clean_baseuris buris =
+  let buris = List.map HGM.strip_trailing_slash buris in
+(*  List.iter prerr_endline buris;*)
   let l = fix [] buris in
   let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
   List.iter MatitaSync.remove l
   
+let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
+

diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli
index f93d6eb96a980121e8d3245e5f242dbf59dcad4f..0de7f586736e4a5080484afe173dd27b1d3b84ba 100644 (file)
--- a/helm/matita/matitacleanLib.mli
+++ b/helm/matita/matitacleanLib.mli
@@ -25,3 +25,9 @@
 
 val clean_baseuris : string list -> unit
 val baseuri_of_file : string -> string 
+
+val baseuri_of_baseuri_decl : ('a, 'b, 'c) TacticAst.statement -> string option
+
+  (** check whether no objects are defined below a given baseuri *)
+val is_empty: string -> bool
+