eval_executable
status mathviewer urichooser user_goal parsed_text script ex
+let fresh_script_id =
+ let i = ref 0 in
+ fun () -> incr i; !i
class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status)
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~urichooser () =
-let std_filename = "unNamed.ma" in
object (self)
- val mutable filename = std_filename
+ val mutable filename = None
+ val scriptId = fresh_script_id ()
+ method private getFilename =
+ match filename with Some f -> f | _ -> assert false
+ method private ppFilename =
+ match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId
initializer
- ignore(GMain.Timeout.add ~ms:20000
+ ignore(GMain.Timeout.add ~ms:30000
~callback:(fun _ -> self#_saveToBackuptFile ();true));
+ set_star self#ppFilename false;
ignore(buffer#connect#modified_changed
(fun _ -> if buffer#modified then
- set_star filename true
+ set_star self#ppFilename true
else
- set_star filename false));
+ set_star self#ppFilename false));
self#reset ()
val mutable statements = []; (** executed statements *)
List.iter (fun o -> o status) observers
method loadFromFile () =
- buffer#set_text (MatitaMisc.input_file filename);
+ buffer#set_text (MatitaMisc.input_file self#getFilename);
self#goto_top;
buffer#set_modified false
method assignFileName file =
- filename <- file;
+ filename <- Some file;
method saveToFile () =
- let oc = open_out filename in
+ let oc = open_out self#getFilename in
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
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")
+ if buffer#modified then
+ begin
+ let f = self#ppFilename ^ "~" 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 " ^ f ^ " saved")
+ end
method private goto_top =
MatitaSync.time_travel ~present:self#status ~past:init;
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);
+ MatitaLog.debug ("Current file name: " ^
+ (match filename with None -> "[ no name ]" | Some f -> f));
end