From 646ade789430669f4a6be3ecbf47d89fe865f132 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jul 2005 10:02:58 +0000 Subject: [PATCH] matita now asks to save .moo if possible or cleans the dust the execution has produced --- helm/matita/Makefile.in | 1 + helm/matita/matitaGui.ml | 123 +++++++++++++++++++++++++++------- helm/matita/matitaScript.ml | 67 +++++++++++++----- helm/matita/matitaScript.mli | 3 + helm/matita/matitacLib.mli | 2 + helm/matita/matitacleanLib.ml | 37 +++++++++- 6 files changed, 188 insertions(+), 45 deletions(-) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index ac2ec13d3..c0c885433 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -32,6 +32,7 @@ CMOS = \ matitacleanLib.cmo \ matitaDisambiguator.cmo \ matitaEngine.cmo \ + matitacLib.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5ac24f8f6..7b73eb112 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -58,6 +58,50 @@ class console ~(buffer: GText.buffer) () = | `Message -> self#message (s ^ "\n") | `Warning -> self#warning (s ^ "\n") end + +let clean_current_baseuri status = + try + let baseuri = MatitaTypes.get_string_option status "baseuri" in + MatitacleanLib.clean_baseuris [baseuri] + with MatitaTypes.Option_error _ -> () + +let ask_and_save_moo_if_needed parent fname status = + let save () = + MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev + in + if (MatitaScript.instance ())#eos then + begin + let mooname = + MatitaMisc.obj_file_of_script fname + in + let rc = + MatitaGtkMisc.ask_confirmation + ~title:"A .moo can be generated" + ~message:(Printf.sprintf + "%s can be generated for %s.\nShould I generate it?" + mooname fname) + ~parent () + in + let b = + match rc with + | `YES -> true + | `NO -> false + | `CANCEL -> raise MatitaTypes.Cancel + in + if b then + save () + else + clean_current_baseuri status + end + else + clean_current_baseuri status + +let ask_unsaved parent = + MatitaGtkMisc.ask_confirmation + ~parent ~title:"Unsaved work!" + ~message:("Your work is unsaved!\n\n"^ + "Do you want to save the script before exiting?") + () class gui () = (* creation order _is_ relevant for windows placement *) @@ -202,17 +246,6 @@ class gui () = script_fname <- None; self#main#saveMenuItem#misc#set_sensitive false in - let loadScript () = - let script = s () in - match self#chooseFile () with - | Some f -> - script#reset (); - script#assignFileName f; - script#loadFromFile (); - console#message ("'"^f^"' loaded.\n"); - self#_enableSaveTo f - | None -> () - in let saveAsScript () = let script = s () in match self#chooseFile ~ok_not_exists:true () with @@ -231,6 +264,31 @@ class gui () = (s ())#saveToFile (); console#message ("'"^f^"' saved.\n"); in + let loadScript () = + let script = s () in + let status = script#status in + try + if source_view#buffer#modified then + begin + match ask_unsaved main#toplevel with + | `YES -> saveScript () + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel + end; + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname status); + match self#chooseFile () with + | Some f -> + script#reset (); + script#assignFileName f; + script#loadFromFile (); + console#message ("'"^f^"' loaded.\n"); + self#_enableSaveTo f + | None -> () + with MatitaTypes.Cancel -> () + in let newScript () = (s ())#reset (); disableSave () in let cursor () = source_buffer#place_cursor @@ -249,23 +307,36 @@ class gui () = in (* quit *) self#setQuitCallback (fun () -> + let status = (MatitaScript.instance ())#status in if source_view#buffer#modified then begin - let rc = - MatitaGtkMisc.ask_confirmation - ~parent:main#toplevel - ~title:"Unsaved work!" - ~message:("Your work is unsaved!\n\n"^ - "Do you want to save the script before exiting?") - () - in - match rc with - | `YES -> saveScript (); - if not source_view#buffer#modified then - GMain.Main.quit () - | `NO -> GMain.Main.quit () - | `CANCEL -> () - end else GMain.Main.quit ()); + let rc = ask_unsaved main#toplevel in + try + match rc with + | `YES -> saveScript (); + if not source_view#buffer#modified then + begin + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed + main#toplevel fname status); + GMain.Main.quit () + end + | `NO -> GMain.Main.quit () + | `CANCEL -> raise MatitaTypes.Cancel + with MatitaTypes.Cancel -> () + end + else + begin + (match script_fname with + | None -> clean_current_baseuri status + | Some fname -> + try + ask_and_save_moo_if_needed main#toplevel fname status; + GMain.Main.quit () + with MatitaTypes.Cancel -> ()) + end); connect_button self#main#scriptAdvanceButton advance; connect_button self#main#scriptRetractButton retract; connect_button self#main#scriptTopButton top; diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 15fe2c9ac..965969a21 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -255,25 +255,28 @@ ask_confirmation user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MD = MatitaDisambiguator in + let module ML = MatitacleanLib in let parsed_text_length = String.length parsed_text in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _) -> - (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)) + (try + (match ML.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)) + with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> eval_macro status mathviewer urichooser parsed_text script mac @@ -479,7 +482,16 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; match pos with | `Top -> self#goto_top; self#notify | `Bottom -> - (try while true do self#_advance () done; self#notify with Margin -> ()) + (try + let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in + let rec dowhile pos = + self#_advance (); + if pos#compare (getpos ()) < 0 then + dowhile (getpos ()) + in + dowhile (getpos ()); + self#notify + with Margin -> ()) | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in @@ -514,6 +526,27 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method proofContext = MatitaMisc.get_proof_context self#status method setGoal n = userGoal <- n + method eos = + let s = self#getFuture in + let rec is_there_and_executable s = + if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + match st with + | TacticAst.Comment (loc,_)-> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let remain_len = String.length s - parsed_text_length in + let next = String.sub s parsed_text_length remain_len in + is_there_and_executable next + | TacticAst.Executable (loc, ex) -> false + in + try + is_there_and_executable s + with + | CicTextualParser2.Parse_error _ -> false + | Margin -> true + + + (* debug *) method dump () = MatitaLog.debug "script status:"; diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index af1c68cc3..43c40b646 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -57,6 +57,9 @@ object method setGoal: int -> unit + (** end of script, true if the whole script has been executed *) + method eos: bool + (* debug *) method dump : unit -> unit diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli index dc24825e5..b19ff5b90 100644 --- a/helm/matita/matitacLib.mli +++ b/helm/matita/matitacLib.mli @@ -28,6 +28,8 @@ val interactive_loop : unit -> unit (** go initializes the status and calls interactive_loop *) val go : unit -> unit val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit + +(** fname is the .ma *) val dump_moo_to_file: string -> string list -> unit (** clean_exit n diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index a616519c1..4218492f4 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -1,3 +1,31 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let debug = false +let debug_prerr = if debug then prerr_endline else ignore + module HGT = Http_getter_types;; module HG = Http_getter;; module HGM = Http_getter_misc;; @@ -116,12 +144,17 @@ let rec fix uris next = | l -> let uris, next = close_uri_list l in fix uris next @ uris let clean_baseuris ?(verbose=true) buris = + Hashtbl.clear cache_of_processed_baseuri; let buris = List.map HGM.strip_trailing_slash buris in - (* List.iter prerr_endline buris; *) + debug_prerr "clean_baseuris called on:"; + if debug then + List.iter debug_prerr 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 (fun u -> prerr_endline (UriManager.string_of_uri u)) l; *) + debug_prerr "clean_baseuri will remove:"; + if debug then + List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; List.iter (MatitaSync.remove ~verbose) l let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = [] -- 2.39.2