X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=d009a63f6f43646846a782265bb276743325e708;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=11b9d1f5299b8698bc8d2ba23216fb7bddbae72e;hpb=3a3199faa15b1d96f8ccd8bd1551f6f4f9aceb66;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 11b9d1f52..d009a63f6 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" ] @@ -139,15 +128,19 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri status = LibraryClean.clean_baseuris [status#baseuri] -let save_moo status = - let script = MatitaScript.current () 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) status - | _ -> clean_current_baseuri 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 = 0 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,7 +761,7 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem ~callback:(function b -> let s = s () in - let status = Interpretations.toggle_active_interpretations s#status b + let _status = Interpretations.toggle_active_interpretations s#status b in assert false (* MATITA 1.0 ??? s#set_grafite_status status*) @@ -841,21 +834,13 @@ class gui () = 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 *) @@ -878,7 +863,7 @@ 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 @@ -887,9 +872,12 @@ class gui () = MatitaMisc.reset_font_size; ignore (main#scriptNotebook#connect#switch_page (fun page -> + let old_script = MatitaScript.at_page current_page in + save_moo0 ~do_clean:false old_script old_script#status; + current_page <- page; let script = MatitaScript.at_page page in script#activate; - main#saveMenuItem#misc#set_sensitive script#has_name)); + main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = let script = MatitaScript.current () in @@ -994,36 +982,19 @@ class gui () = method newScript () = let scrolledWindow = GBin.scrolled_window () in let hbox = GPack.hbox () in - let tab_label = GMisc.label ~text:"foo" - ~packing:hbox#pack () 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 + let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in closebutton#set_image image#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 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 hbox#coerce) script)); + self#closeScript + (main#scriptNotebook#page_num scrolledWindow#coerce) script)); main#scriptNotebook#goto_page 0; sequents_viewer#reset; sequents_viewer#load_logo; @@ -1074,35 +1045,9 @@ class gui () = 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 private 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 private setQuitCallback callback = @@ -1130,9 +1075,10 @@ class gui () = 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 @@ -1190,66 +1136,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;*)