From a956992315e3a723c69dff5edc361ea3db75cd54 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Jun 2005 15:32:48 +0000 Subject: [PATCH] added autosave and * (modified feature) --- helm/matita/matita.glade | 2 +- helm/matita/matita.ml | 1 + helm/matita/matitaGui.ml | 19 ++++++++--- helm/matita/matitaGui.mli | 1 + helm/matita/matitaScript.ml | 63 +++++++++++++++++++++++++++--------- helm/matita/matitaScript.mli | 6 ++-- helm/matita/tests/rewrite.ma | 3 +- 7 files changed, 71 insertions(+), 24 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 47d8a3d1e..98526c578 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1970,7 +1970,7 @@ Copyright (C) 2005, - + True script False diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 40592d001..6e2fe2526 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -86,6 +86,7 @@ let script = ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n")) () ~id:"boh?" uris with MatitaTypes.Cancel -> []) + ~set_star:gui#setStar () (* math viewers *) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e2b4d4682..1e2b54826 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -211,7 +211,8 @@ class gui () = match self#chooseFile () with | Some f -> script#reset (); - script#loadFrom f; + script#assignFileName f; + script#loadFromFile (); console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f | None -> () @@ -220,7 +221,8 @@ class gui () = let script = s () in match self#chooseFile ~ok_not_exists:true () with | Some f -> - script#saveTo f; + script#assignFileName f; + script#saveToFile (); console#message ("'"^f^"' saved.\n"); self#_enableSaveTo f | None -> () @@ -229,7 +231,8 @@ class gui () = match script_fname with | None -> saveAsScript () | Some f -> - (s ())#saveTo f; + (s ())#assignFileName f; + (s ())#saveToFile (); console#message ("'"^f^"' saved.\n"); in let newScript () = (s ())#reset (); disableSave () in @@ -293,9 +296,17 @@ class gui () = method loadScript file = let script = MatitaScript.instance () in script#reset (); - script#loadFrom file; + script#assignFileName file; + script#loadFromFile (); console#message ("'"^file^"' loaded."); self#_enableSaveTo file + + method setStar name b = + let l = main#scriptLabel in + if b then + l#set_text (name ^ " *") + else + l#set_text (name) method private _enableSaveTo file = script_fname <- Some file; diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 80c183fac..18fe33016 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -77,6 +77,7 @@ object method askText: ?title:string -> ?msg:string -> unit -> string option method loadScript: string -> unit + method setStar: string -> bool -> unit (** {3 Fonts} *) method increaseFontSize: unit -> unit diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 1f8add6a0..043fc31e4 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -291,9 +291,21 @@ user_goal script s = class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) + ~set_star ~urichooser () = +let std_filename = "unNamed.ma" in object (self) - initializer self#reset () + val mutable filename = std_filename + + initializer + ignore(GMain.Timeout.add ~ms:20000 + ~callback:(fun _ -> self#_saveToBackuptFile ();true)); + ignore(buffer#connect#modified_changed + (fun _ -> if buffer#modified then + set_star filename true + else + set_star filename false)); + self#reset () val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -305,6 +317,7 @@ object (self) (** goal as seen by the user (i.e. metano corresponding to current tab) *) val mutable userGoal = ~-1 + (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter @@ -327,12 +340,16 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; history <- List.rev new_statuses @ history; statements <- List.rev new_statements @ statements; let start = buffer#get_iter_at_mark (`MARK locked_mark) in - if statement = None then begin - let stop = start#copy#forward_chars parsed_len in - buffer#delete ~start ~stop - end; let new_text = String.concat "" new_statements in - buffer#insert ~iter:start new_text; + if new_text <> String.sub s 0 parsed_len then + begin +(* prerr_endline ("new:" ^ new_text); *) +(* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *) + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; +(* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *) + end; self#moveMark (String.length new_text) method private _retract () = @@ -381,16 +398,29 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let status = self#status in List.iter (fun o -> o status) observers - method loadFrom fname = - buffer#set_text (MatitaMisc.input_file fname); - self#goto_top - - method saveTo fname = - let oc = open_out fname in + method loadFromFile () = + buffer#set_text (MatitaMisc.input_file filename); + self#goto_top; + buffer#set_modified false + + method assignFileName file = + filename <- file; + + method saveToFile () = + let oc = open_out filename in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); - close_out oc - + close_out oc; + buffer#set_modified false + + method private _saveToBackuptFile () = + let f = filename ^ "~" in + let oc = open_out f in + output_string oc (buffer#get_text ~start:buffer#start_iter + ~stop:buffer#end_iter ()); + close_out oc; + MatitaLog.debug ("backup file " ^ f ^ " saved") + method private goto_top = MatitaSync.time_travel ~present:self#status ~past:init; statements <- []; @@ -449,13 +479,14 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); MatitaLog.debug (sprintf "%d statements:" (List.length statements)); List.iter MatitaLog.debug statements; + MatitaLog.debug ("Current file name: " ^ filename); end let _script = ref None -let script ~buffer ~init ~mathviewer ~urichooser () = - let s = new script ~buffer ~init ~mathviewer ~urichooser () in +let script ~buffer ~init ~mathviewer ~urichooser ~set_star () = + let s = new script ~buffer ~init ~mathviewer ~urichooser ~set_star () in _script := Some s; s diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index b6b3d8ae2..6aea4ad1c 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -42,8 +42,9 @@ object (** {2 Load/save} *) - method loadFrom : string -> unit - method saveTo : string -> unit + method assignFileName : string -> unit (* to the current active file *) + method loadFromFile : unit -> unit + method saveToFile : unit -> unit (** {2 Current proof} (if any) *) @@ -66,6 +67,7 @@ val script: init:MatitaTypes.status -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> + set_star: (string -> bool -> unit) -> unit -> script diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 72e80987d..da93e1e52 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -1,6 +1,6 @@ alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "leibnitz's equality". alias symbol "plus" (instance 0) = "natural plus". @@ -18,3 +18,4 @@ rewrite right H in \vdash (? ? ? (% ?)). simplify. reflexivity. qed. + \ No newline at end of file -- 2.39.2