From c1902bcdefa7ef7770e470a49fc778f8846cca62 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 22 Jul 2005 16:51:18 +0000 Subject: [PATCH] When matita is started on a non-existent file, it avoids creating it immediately! --- helm/matita/matita.txt | 7 ++----- helm/matita/matitaGui.ml | 23 ++++++++++------------- helm/matita/matitaScript.ml | 4 ++-- helm/matita/matitaScript.mli | 2 +- 4 files changed, 15 insertions(+), 21 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 23bd0c42e..19c78922f 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -59,8 +59,6 @@ TODO - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare - - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza - salvare. In verita' foo e' stato scritto lo stesso! - sensitiveness per copy/paste/cut/delete nel menu Edit - sensitiveness per goto begin/end/etc. @@ -79,12 +77,11 @@ TODO - matitamake foo/a.ma non funziona; bisogna chiamarlo con matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack - - copiare nel .moo la baseuri e poi il matitaclean la legge da li e non dal - .ma (si evita il syntax error e il cambio di una baseuri non causa - sporcizia) - non chiudere transitivamente i moo ?? DONE +- fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza + salvare. In verita' foo e' stato scritto lo stesso! -> CSC - matitaclean deve rimuovere anche i .moo; in alternativa il makefile non deve basarsi sui .moo per decidere se qualcosa e' stato compilato o meno -> CSC, Gares diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8dc0cf313..108b36bfb 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -596,7 +596,7 @@ class gui () = script#reset (); script#assignFileName f; source_view#source_buffer#begin_not_undoable_action (); - script#loadFromFile (); + script#loadFromFile f; source_view#source_buffer#end_not_undoable_action (); console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f @@ -713,18 +713,15 @@ class gui () = let script = MatitaScript.instance () in script#reset (); script#assignFileName file; - if not (Sys.file_exists file) then - begin - let oc = open_out file in - let template = MatitaMisc.input_file BuildTimeConf.script_template in - output_string oc template; - close_out oc - end; - source_view#source_buffer#begin_not_undoable_action (); - script#loadFromFile (); - source_view#source_buffer#end_not_undoable_action (); - console#message ("'"^file^"' loaded."); - self#_enableSaveTo file + let content = + if Sys.file_exists file then file + else BuildTimeConf.script_template + in + source_view#source_buffer#begin_not_undoable_action (); + script#loadFromFile content; + source_view#source_buffer#end_not_undoable_action (); + console#message ("'"^file^"' loaded."); + self#_enableSaveTo file method setStar name b = let l = main#scriptLabel in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index f339ebb40..ad1530d4e 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -542,8 +542,8 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let status = self#status in List.iter (fun o -> o status) observers - method loadFromFile () = - buffer#set_text (MatitaMisc.input_file self#getFilename); + method loadFromFile f = + buffer#set_text (MatitaMisc.input_file f); self#goto_top; buffer#set_modified false diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 5266a61e0..258a72e0c 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -46,7 +46,7 @@ object (** {2 Load/save} *) method assignFileName : string -> unit (* to the current active file *) - method loadFromFile : unit -> unit + method loadFromFile : string -> unit method saveToFile : unit -> unit (** {2 Current proof} (if any) *) -- 2.39.2