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