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 -> ()
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 -> ()
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
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;
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 ];
(** 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
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 () =
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 <- [];
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