From: Enrico Tassi Date: Mon, 4 Jul 2005 13:43:05 +0000 (+0000) Subject: aded confirmation dialog for baseuri redefinement X-Git-Tag: PRE_GETTER_STORAGE~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fa3a1e91d8a1e647775ca101255633ba265a9f2;p=helm.git aded confirmation dialog for baseuri redefinement --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 93441ed83..3eb0fc6a1 100644 --- 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 f913639f9..2151541a3 100644 --- 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 9ca48d9ca..4f7027d61 100644 --- 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 677006b71..af1c68cc3 100644 --- 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 76ec992be..8f8a66e09 100644 --- 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 992443a35..f8376416e 100644 --- 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 f93d6eb96..0de7f5867 100644 --- 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 +