From 5d8d825b9bf6b3cf346ba8e81ffd0ac1e1902ecb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Dec 2010 13:14:15 +0000 Subject: [PATCH] First steps towards a multi-document interface. --- matita/matita/matita.glade | 31 +++-------------------- matita/matita/matita.ml | 1 - matita/matita/matitaGui.ml | 18 +------------- matita/matita/matitaGuiTypes.mli | 1 - matita/matita/matitaScript.ml | 42 +++++++++++++++++++------------- matita/matita/matitaScript.mli | 5 +--- 6 files changed, 31 insertions(+), 67 deletions(-) diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade index f7be5eab3..6d4b59672 100644 --- a/matita/matita/matita.glade +++ b/matita/matita/matita.glade @@ -1679,7 +1679,7 @@ True True - bottom + True True @@ -1702,35 +1702,11 @@ - - True - True - automatic - automatic - - - True - - - True - Not implemented. - - - - - - - 1 - + - - True - outline - + - 1 - False tab @@ -1761,6 +1737,7 @@ True True + True False diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 4b8548f19..ee20eda89 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -59,7 +59,6 @@ let script = ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n")) () ~id:"boh?" uris with MatitaTypes.Cancel -> []) - ~set_star:gui#setStar ~ask_confirmation: (fun ~title ~message -> MatitaGtkMisc.ask_confirmation ~title ~message diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index cd9603f85..7589f19f8 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -839,10 +839,6 @@ class gui () = "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); - (* TO BE REMOVED *) - main#scriptNotebook#remove_page 1; - main#scriptNotebook#set_show_tabs false; - (* / TO BE REMOVED *) let module Hr = Helm_registry in MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem ~callback:(function @@ -934,8 +930,7 @@ class gui () = (s ())#reset (); (s ())#template (); source_view#source_buffer#end_not_undoable_action (); - disableSave (); - (s ())#assignFileName None + disableSave () in let cursor () = source_buffer#place_cursor @@ -1262,17 +1257,6 @@ class gui () = console#message ("'"^file^"' loaded."); self#_enableSaveTo file - method setStar b = - let s = MatitaScript.current () in - let w = main#toplevel in - let set x = w#set_title x in - let name = - "Matita - " ^ Filename.basename s#filename ^ - (if b then "*" else "") ^ - " in " ^ s#buri_of_current_file - in - set name - method private _enableSaveTo file = self#main#saveMenuItem#misc#set_sensitive true diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 9b2ed087c..f10c0201b 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -90,7 +90,6 @@ object method askText: ?title:string -> ?msg:string -> unit -> string option method loadScript: string -> unit - method setStar: bool -> unit (** {3 Fonts} *) method increaseFontSize: unit -> unit diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 02f9a23b0..75d995f78 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -246,7 +246,6 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView2.source_view) - ~set_star ~ask_confirmation ~urichooser () = @@ -323,7 +322,7 @@ object (self) ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); ignore (buffer#connect#modified_changed - (fun _ -> set_star buffer#modified)) + (fun _ -> self#set_star buffer#modified)) val mutable statements = [] (** executed statements *) @@ -511,17 +510,26 @@ object (self) buffer#set_modified false method assignFileName file = - let file = - match file with - | Some f -> Some (Librarian.absolutize f) - | None -> None - in - filename_ <- file; - include_paths_ <- - (match file with Some file -> read_include_paths file | None -> []); - self#reset_buffer; - Sys.chdir self#curdir; - HLog.debug ("Moving to " ^ Sys.getcwd ()) + match file with + None -> + (MatitaMisc.get_gui ())#main#scriptLabel#set_text default_fname; + filename_ <- None; + include_paths_ <- []; + self#reset_buffer + | Some file -> + let f = Librarian.absolutize file in + (MatitaMisc.get_gui ())#main#scriptLabel#set_text (Filename.basename f); + filename_ <- Some f; + include_paths_ <- read_include_paths f; + self#reset_buffer; + Sys.chdir self#curdir; + HLog.debug ("Moving to " ^ Sys.getcwd ()) + + method set_star b = + let label = (MatitaMisc.get_gui ())#main#scriptLabel in + label#set_text ((if b then "*" else "") ^ Filename.basename self#filename); + label#misc#set_tooltip_text + ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename) method saveToFile () = if self#has_name then @@ -529,7 +537,7 @@ object (self) output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - set_star false; + self#set_star false; buffer#set_modified false else HLog.error "Can't save, no filename selected" @@ -564,7 +572,7 @@ object (self) let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; - set_star false + self#set_star false method goto (pos: [`Top | `Bottom | `Cursor]) () = try @@ -694,9 +702,9 @@ end let _script = ref None -let script ~source_view ~urichooser ~ask_confirmation ~set_star () +let script ~source_view ~urichooser ~ask_confirmation () = - let s = new script ~source_view ~ask_confirmation ~urichooser ~set_star () in + let s = new script ~source_view ~ask_confirmation ~urichooser () in _script := Some s; s diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index de95aac52..02e06d2d1 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -59,7 +59,6 @@ object method loadFromFile : string -> unit method loadFromString : string -> unit method saveToFile : unit -> unit - method filename : string (** {2 Current proof} (if any) *) @@ -74,6 +73,7 @@ object (** misc *) method clean_dirty_lock: unit + method set_star: bool -> unit (* debug *) method dump : unit -> unit @@ -81,14 +81,11 @@ object end - (** @param set_star callback used to set the modified symbol (usually a star - * "*") on the side of a script name *) val script: source_view:GSourceView2.source_view -> urichooser: (NReference.reference list -> NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> - set_star: (bool -> unit) -> unit -> script -- 2.39.2