X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=94e3e751db0f046b2f27cf01f36ca761b8fb202e;hb=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;hp=91276e0ddf8945c1e9c24e7ff6c7107f0a24da08;hpb=0c69106b8cf67a0baad545a9d7b0816b2b7de8ac;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 91276e0dd..94e3e751d 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -35,8 +35,6 @@ exception Found of int let all_disambiguation_passes = ref false -let gui_instance = ref None - (* this is a shit and should be changed :-{ *) let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") @@ -45,13 +43,12 @@ let interactive_uri_choice ?copy_cb () ~id uris = - let gui = MatitaMisc.get_gui () in if (selection_mode <> `SINGLE) && (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") then uris else begin - let dialog = gui#newUriDialog () in + let dialog = new uriChoiceDialog () in if hide_uri_entry then dialog#uriEntryHBox#misc#hide (); if hide_try then @@ -107,14 +104,6 @@ let interactive_uri_choice end -class type browserWin = - (* this class exists only because GEdit.combo_box_entry is not supported by - * lablgladecc :-(((( *) -object - inherit MatitaGeneratedGui.browserWin - method browserUri: GEdit.entry -end - class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] @@ -136,18 +125,22 @@ 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 script = MatitaScript.current () in - let baseuri = grafite_status#baseuri in +let save_moo0 ~do_clean script status = + 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 + | _ -> if do_clean then clean_current_baseuri status +;; + +let save_moo status = + let script = MatitaScript.current () in + save_moo0 ~do_clean:true script status ;; let ask_unsaved parent filename = @@ -326,7 +319,6 @@ let interactive_error_interp ~all_passes (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> let dialog = new disambiguationErrors () in - dialog#check_widgets (); if all_passes then dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false; let model = new interpErrorModel dialog#treeview choices in @@ -427,23 +419,24 @@ class gui () = val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false + val mutable current_page = -1 initializer let s () = MatitaScript.current () in - (* glade's check widgets *) - List.iter (fun w -> w#check_widgets ()) - (let c w = (w :> unit>) in - [ c fileSel; c main; c findRepl]); (* key bindings *) List.iter (* global key bindings *) - (fun (key, callback) -> self#addKeyBinding key callback) + (fun (key, modifiers, callback) -> + self#addKeyBinding key ~modifiers callback) (* [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, toggle_win ~check:main#showCheckMenuItem check#checkWin; *) - [ ]; + [ + GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page; + GdkKeysyms._Page_Up, [`CONTROL], main#scriptNotebook#previous_page + ]; (* about win *) let parse_txt_file file = let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in @@ -605,7 +598,7 @@ class gui () = match !id with | None -> assert false (* a race condition occurred *) | Some id -> - (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id)); + source_view#source_buffer#misc#disconnect id)); source_view#source_buffer#place_cursor (source_view#source_buffer#get_iter (`OFFSET x')); end; @@ -768,8 +761,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*) @@ -782,7 +774,7 @@ class gui () = main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) - HLog.set_log_callback self#console#log_callback; + HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg); GtkSignal.user_handler := (function | MatitaScript.ActionCancelled s -> HLog.error s @@ -792,26 +784,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 +811,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,26 +828,19 @@ 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 - c#load (`About `Coercions)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions))); connect_menu_item main#showHintsDbMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Hints)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints))); connect_menu_item main#showTermGrammarMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Grammar)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar))); connect_menu_item main#showUnicodeTable - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `TeX)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX))); (* debug menu *) main#debugMenu#misc#hide (); (* HBUGS *) @@ -907,13 +863,19 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* math view handling *) connect_menu_item main#newCicBrowserMenuItem (fun () -> - ignore(MatitaMathView.cicBrowser ())); + ignore(MatitaMathView.cicBrowser None)); connect_menu_item main#increaseFontSizeMenuItem MatitaMisc.increase_font_size; connect_menu_item main#decreaseFontSizeMenuItem MatitaMisc.decrease_font_size; connect_menu_item main#normalFontSizeMenuItem MatitaMisc.reset_font_size; + ignore (main#scriptNotebook#connect#switch_page (fun page -> + self#save_page (); + current_page <- 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 @@ -972,53 +934,96 @@ 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 private save_page () = + if current_page >= 0 then + let old_script = MatitaScript.at_page current_page in + save_moo0 ~do_clean:false old_script old_script#status + method newScript () = + self#save_page (); let scrolledWindow = GBin.scrolled_window () in - let tab_label = GMisc.label ~text:"foo" () in - ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce); - let script = - MatitaScript.script - ~urichooser:(fun source_view uris -> - try - interactive_uri_choice ~selection_mode:`SINGLE - ~title:"Matita: URI chooser" - ~msg:"Select the URI" ~hide_uri_entry:true - ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT - ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n")) - () ~id:"boh?" uris - with MatitaTypes.Cancel -> []) - ~ask_confirmation: - (fun ~title ~message -> - MatitaGtkMisc.ask_confirmation ~title ~message - ~parent:(MatitaMisc.get_gui ())#main#toplevel ()) - ~parent:scrolledWindow ~tab_label () - 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 ~parent:scrolledWindow ~tab_label () in + ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce + scrolledWindow#coerce); + ignore (closebutton#connect#clicked (fun () -> + self#closeScript + (main#scriptNotebook#page_num scrolledWindow#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 (); @@ -1039,49 +1044,23 @@ 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 () = - object (self) - inherit browserWin () - val combo = GEdit.entry () - initializer - self#check_widgets (); - let combo_widget = combo#coerce in - uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; - combo#misc#grab_focus () - method browserUri = combo - end - - method newUriDialog () = - let dialog = new uriChoiceDialog () in - dialog#check_widgets (); - dialog - - method newConfirmationDialog () = - let dialog = new confirmationDialog () in - dialog#check_widgets (); - dialog - - method newEmptyDialog () = - let dialog = new emptyDialog () in - dialog#check_widgets (); - dialog - - method private addKeyBinding key callback = - List.iter (fun evbox -> add_key_binding key callback evbox) + method private addKeyBinding key ?modifiers callback = +(* List.iter (fun evbox -> add_key_binding key callback evbox) *) + List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback) 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 (); @@ -1096,32 +1075,14 @@ 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 () = let g = new gui () in - gui_instance := Some g; - MatitaMisc.set_gui g; - g + let rg = (g :> MatitaGuiTypes.gui) in + MatitaMisc.set_gui rg; + g#newScript (); + rg let instance = singleton gui @@ -1179,66 +1140,65 @@ class interpModel = let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris = - let gui = instance () in - let dialog = gui#newUriDialog () in - dialog#uriEntryHBox#misc#hide (); - dialog#uriChoiceSelectedButton#misc#hide (); - dialog#uriChoiceAutoButton#misc#hide (); - dialog#uriChoiceConstantsButton#misc#hide (); - dialog#uriChoiceTreeView#selection#set_mode - (`SINGLE :> Gtk.Tags.selection_mode); - let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in - dialog#uriChoiceDialog#set_title title; - let hack_len = MatitaGtkMisc.utf8_string_length text in - let rec colorize acc_len = function - | [] -> - let floc = HExtlib.floc_of_loc (acc_len,hack_len) in - escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) - | he::tl -> - let start, stop = HExtlib.loc_of_floc he in - let floc1 = HExtlib.floc_of_loc (acc_len,start) in - let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in - let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in - escape_pango_markup str1 ^ "" ^ - escape_pango_markup str2 ^ "" ^ - colorize stop tl - in + let dialog = new uriChoiceDialog () in + dialog#uriEntryHBox#misc#hide (); + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceAutoButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + dialog#uriChoiceTreeView#selection#set_mode + (`SINGLE :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + dialog#uriChoiceDialog#set_title title; + let hack_len = MatitaGtkMisc.utf8_string_length text in + let rec colorize acc_len = function + | [] -> + let floc = HExtlib.floc_of_loc (acc_len,hack_len) in + escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) + | he::tl -> + let start, stop = HExtlib.loc_of_floc he in + let floc1 = HExtlib.floc_of_loc (acc_len,start) in + let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in + let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in + escape_pango_markup str1 ^ "" ^ + escape_pango_markup str2 ^ "" ^ + colorize stop tl + in (* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in - Printf.eprintf "(%d,%d)" start stop) locs; *) - let locs = - List.sort - (fun loc1 loc2 -> - fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) - locs - in + Printf.eprintf "(%d,%d)" start stop) locs; *) + let locs = + List.sort + (fun loc1 loc2 -> + fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) + locs + in (* prerr_endline "XXXXXXXXXXXXXXXXXXXX"; - List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in - Printf.eprintf "(%d,%d)" start stop) locs; - prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) - dialog#uriChoiceLabel#set_use_markup true; - let txt = colorize 0 locs in - let txt,_ = MatitaGtkMisc.utf8_parsed_text txt - (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) - in - dialog#uriChoiceLabel#set_label txt; - List.iter model#easy_append uris; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#uriChoiceForwardButton (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some uris)); - connect_button dialog#uriChoiceAbortButton (fun _ -> return None); - dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise MatitaTypes.Cancel - | Some uris -> uris) + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; + prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) + dialog#uriChoiceLabel#set_use_markup true; + let txt = colorize 0 locs in + let txt,_ = MatitaGtkMisc.utf8_parsed_text txt + (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) + in + dialog#uriChoiceLabel#set_label txt; + List.iter model#easy_append uris; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceForwardButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) let interactive_interp_choice () text prefix_len choices = (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)