X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FmatitaGui.ml;h=11b9d1f5299b8698bc8d2ba23216fb7bddbae72e;hb=3a3199faa15b1d96f8ccd8bd1551f6f4f9aceb66;hp=eb39e019ddfc54472aa457d0eedb648adc8dd42c;hpb=65a0f081b506782b436bcac976343261b8011eba;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index eb39e019d..11b9d1f52 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -136,18 +136,18 @@ class console ~(buffer: GText.buffer) () = | `Warning -> self#warning (s ^ "\n") end -let clean_current_baseuri grafite_status = - LibraryClean.clean_baseuris [grafite_status#baseuri] +let clean_current_baseuri status = + LibraryClean.clean_baseuris [status#baseuri] -let save_moo grafite_status = +let save_moo status = let script = MatitaScript.current () in - let baseuri = grafite_status#baseuri in + let baseuri = status#baseuri in match script#bos, script#eos with | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - grafite_status - | _ -> clean_current_baseuri grafite_status + status + | _ -> clean_current_baseuri status ;; let ask_unsaved parent filename = @@ -768,8 +768,7 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem ~callback:(function b -> let s = s () in - let status = - Interpretations.toggle_active_interpretations s#grafite_status b + let status = Interpretations.toggle_active_interpretations s#status b in assert false (* MATITA 1.0 ??? s#set_grafite_status status*) @@ -792,26 +791,6 @@ class gui () = can we do? *) notify_exn (MatitaScript.current ())#source_view exn else raise exn); - let disableSave () = - (s())#assignFileName None; - main#saveMenuItem#misc#set_sensitive false - in - let saveAsScript script = - match self#chooseFile ~ok_not_exists:true () with - | Some f -> - HExtlib.touch f; - script#assignFileName (Some f); - script#saveToFile (); - console#message ("'"^f^"' saved.\n"); - self#_enableSaveTo f - | None -> () - in - let saveScript script = - if script#has_name then - (script#saveToFile (); - console#message ("'"^script#filename^"' saved.\n")) - else saveAsScript script - in let loadScript () = try match self#chooseFile () with @@ -839,17 +818,8 @@ class gui () = MatitaScript.iter_scripts (fun script -> if not !cancel then - if script#source_view#buffer#modified then - match - ask_unsaved main#toplevel (Filename.basename script#filename) - with - | `YES -> - saveScript script; - save_moo script#grafite_status - | `NO -> () - | `CANCEL -> cancel := true - else - save_moo script#grafite_status); + if not (self#closeScript0 script) then + cancel := true); if not !cancel then GMain.Main.quit ()); connect_button main#scriptAdvanceButton advance; @@ -865,10 +835,11 @@ class gui () = connect_menu_item main#scriptJumpMenuItem jump; connect_menu_item main#openMenuItem loadScript; connect_menu_item main#saveMenuItem - (fun () -> saveScript (MatitaScript.current ())); + (fun () -> self#saveScript (MatitaScript.current ())); connect_menu_item main#saveAsMenuItem - (fun () -> saveAsScript (MatitaScript.current ())); - connect_menu_item main#newMenuItem self#newScript; + (fun () -> self#saveAsScript (MatitaScript.current ())); + connect_menu_item main#newMenuItem self#newScript; + connect_menu_item main#closeMenuItem self#closeCurrentScript; connect_menu_item main#showCoercionsGraphMenuItem (fun _ -> let c = MatitaMathView.cicBrowser () in @@ -915,7 +886,10 @@ class gui () = connect_menu_item main#normalFontSizeMenuItem MatitaMisc.reset_font_size; ignore (main#scriptNotebook#connect#switch_page - (fun page -> (MatitaScript.at_page page)#activate)); + (fun page -> + let script = MatitaScript.at_page page in + script#activate; + main#saveMenuItem#misc#set_sensitive script#has_name)); method private externalEditor () = let script = MatitaScript.current () in @@ -974,9 +948,61 @@ class gui () = | Exit -> () | Invalid_argument _ -> script#goto `Bottom () + method private saveAsScript script = + match self#chooseFile ~ok_not_exists:true () with + | Some f -> + HExtlib.touch f; + script#assignFileName (Some f); + script#saveToFile (); + console#message ("'"^f^"' saved.\n"); + self#_enableSaveTo f + | None -> () + + method private saveScript script = + if script#has_name then + (script#saveToFile (); + console#message ("'"^script#filename^"' saved.\n")) + else self#saveAsScript script + + (* returns false if closure is aborted by the user *) + method private closeScript0 script = + if script#source_view#buffer#modified then + match + ask_unsaved main#toplevel (Filename.basename script#filename) + with + | `YES -> + self#saveScript script; + save_moo script#status; + true + | `NO -> true + | `CANCEL -> false + else + (save_moo script#status; true) + + method private closeScript page script = + if self#closeScript0 script then + begin + MatitaScript.destroy page; + ignore (main#scriptNotebook#remove_page page) + end + + method private closeCurrentScript () = + let page = main#scriptNotebook#current_page in + let script = MatitaScript.at_page page in + self#closeScript page script + method newScript () = let scrolledWindow = GBin.scrolled_window () in - let tab_label = GMisc.label ~text:"foo" () in + let hbox = GPack.hbox () in + let tab_label = GMisc.label ~text:"foo" + ~packing:hbox#pack () in + let _ = + GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in + let closebutton = + GButton.button ~relief:`NONE ~packing:hbox#pack () in + let image = + GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in + closebutton#set_image image#coerce; let script = MatitaScript.script ~urichooser:(fun source_view uris -> @@ -994,33 +1020,35 @@ class gui () = ~parent:(MatitaMisc.get_gui ())#main#toplevel ()) ~parent:scrolledWindow ~tab_label () in - ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce); + ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce + scrolledWindow#coerce); + ignore (closebutton#connect#clicked (fun () -> + self#closeScript (main#scriptNotebook#page_num hbox#coerce) script)); main#scriptNotebook#goto_page 0; sequents_viewer#reset; sequents_viewer#load_logo; let browser_observer _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer grafite_status = + let sequents_observer status = sequents_viewer#reset; - match grafite_status#ng_mode with + match status#ng_mode with `ProofMode -> - sequents_viewer#nload_sequents grafite_status; + sequents_viewer#nload_sequents status; (try - script#setGoal - (Some (Continuationals.Stack.find_goal grafite_status#stack)); let goal = - match script#goal with - None -> assert false - | Some n -> n + Continuationals.Stack.find_goal status#stack in - sequents_viewer#goto_sequent grafite_status goal - with Failure _ -> script#setGoal None); + sequents_viewer#goto_sequent status goal + with Failure _ -> ()); | `CommandMode -> sequents_viewer#load_logo in script#addObserver sequents_observer; script#addObserver browser_observer method loadScript file = - self#newScript (); + let page = main#scriptNotebook#current_page in + let script = MatitaScript.at_page page in + if script#source_view#buffer#modified || script#has_name then + self#newScript (); let script = MatitaScript.current () in let source_view = script#source_view in script#reset (); @@ -1041,9 +1069,9 @@ class gui () = method private _enableSaveTo file = self#main#saveMenuItem#misc#set_sensitive true - method console = console - method fileSel = fileSel - method findRepl = findRepl + method private console = console + method private fileSel = fileSel + method private findRepl = findRepl method main = main method newBrowserWin () = @@ -1063,7 +1091,7 @@ class gui () = dialog#check_widgets (); dialog - method newConfirmationDialog () = + method private newConfirmationDialog () = let dialog = new confirmationDialog () in dialog#check_widgets (); dialog @@ -1077,13 +1105,13 @@ class gui () = List.iter (fun evbox -> add_key_binding key callback evbox) keyBindingBoxes - method setQuitCallback callback = + method private setQuitCallback callback = connect_menu_item main#quitMenuItem callback; ignore (main#toplevel#event#connect#delete (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback - method chooseFile ?(ok_not_exists = false) () = + method private chooseFile ?(ok_not_exists = false) () = _ok_not_exists <- ok_not_exists; _only_directory <- false; fileSel#fileSelectionWin#show (); @@ -1098,25 +1126,6 @@ class gui () = (* we should check that this is a directory *) chosen_file - method askText ?(title = "") ?(msg = "") () = - let dialog = new textDialog () in - dialog#textDialog#set_title title; - dialog#textDialogLabel#set_label msg; - let text = ref None in - let return v = - text := v; - dialog#textDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#textDialogCancelButton (fun _ -> return None); - connect_button dialog#textDialogOkButton (fun _ -> - let text = dialog#textDialogTextView#buffer#get_text () in - return (Some text)); - dialog#textDialog#show (); - GtkThread.main (); - !text - end let gui () =