X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=34238f80d4e66cb199d7c0f232f4b6dfb0c29f65;hb=dab3163daed8034aca17b9ed18d5200e4b9f046a;hp=ec4d042ff38223eb61cd6151c84b7f19171c8d99;hpb=716da638633f01d6a5b52c05e0bd6adc86385b60;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index ec4d042ff..34238f80d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -31,6 +31,14 @@ open MatitaMisc let gui_instance = ref None ;; +class type browserWin = + (* this class exists only because GEdit.combo_box_entry is not supported by + * lablgladecc :-(((( *) +object + inherit MatitaGeneratedGui.browserWin + method browserUri: GEdit.combo_box_entry +end + class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] @@ -63,7 +71,8 @@ class gui () = object (self) val mutable chosen_file = None val mutable _ok_not_exists = false - + val mutable script_fname = None + initializer (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) @@ -155,33 +164,37 @@ class gui () = (sprintf "Uncaught exception: %s" (Printexc.to_string exn))); (* script *) let s () = MatitaScript.instance () in - let script_fname = ref None in - let enable_save_to f = - script_fname := Some f; - self#main#saveMenuItem#misc#set_sensitive true - in - let disable_save () = - script_fname := None; + let disableSave () = + script_fname <- None; self#main#saveMenuItem#misc#set_sensitive false in let loadScript () = let script = s () in match self#chooseFile () with - | Some f -> script#reset (); script#loadFrom f; enable_save_to f + | Some f -> + script#reset (); + script#loadFrom f; + console#message ("'"^f^"' loaded."); + self#_enableSaveTo f | None -> () in let saveAsScript () = let script = s () in match self#chooseFile ~ok_not_exists:true () with - | Some f -> script#saveTo f; enable_save_to f + | Some f -> + script#saveTo f; + console#message ("'"^f^"' saved.\n"); + self#_enableSaveTo f | None -> () in let saveScript () = - match !script_fname with + match script_fname with | None -> saveAsScript () - | Some f -> (s ())#saveTo f + | Some f -> + (s ())#saveTo f; + console#message ("'"^f^"' saved.\n"); in - let newScript () = (s ())#reset (); disable_save () in + let newScript () = (s ())#reset (); disableSave () in let cursor () = let buf = self#main#scriptTextView#buffer in buf#place_cursor (buf#get_iter_at_mark (`NAME "locked")) @@ -220,14 +233,48 @@ class gui () = let buf = self#main#scriptTextView#buffer in buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n"; advance ()); + (* script monospace font stuff *) + let font = + Helm_registry.get_opt_default Helm_registry.get + BuildTimeConf.default_script_font "matita.script_font" + in +(* let monospace_tag = + self#main#scriptTextView#buffer#create_tag [`FONT_DESC font] + in *) + self#main#scriptTextView#misc#modify_font_by_name font; +(* let _ = + self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ -> + let start, stop = self#main#scriptTextView#buffer#bounds in + self#main#scriptTextView#buffer#apply_tag monospace_tag start stop) + in *) (* debug menu *) self#main#debugMenu#misc#hide (); (* status bar *) - self#main#hintLowImage#set_file "icons/matita-bulb-low.png"; - self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png"; - self#main#hintHighImage#set_file "icons/matita-bulb-high.png"; + self#main#hintLowImage#set_file (image_path "matita-bulb-low.png"); + self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); + self#main#hintHighImage#set_file (image_path "matita-bulb-high.png"); (* focus *) - self#main#scriptTextView#misc#grab_focus () + self#main#scriptTextView#misc#grab_focus (); + (* main win dimension *) + let width = Gdk.Screen.width () in + let height = Gdk.Screen.height () in + let main_w = width * 90 / 100 in + let main_h = height * 80 / 100 in + let script_w = main_w / 2 in + self#main#toplevel#resize ~width:main_w ~height:main_h; + self#main#hpaneScriptSequent#set_position script_w + + method loadScript file = + let script = MatitaScript.instance () in + script#reset (); + script#loadFrom file; + console#message ("'"^file^"' loaded."); + self#_enableSaveTo file + + method private _enableSaveTo file = + script_fname <- Some file; + self#main#saveMenuItem#misc#set_sensitive true + method console = console @@ -236,9 +283,15 @@ class gui () = method main = main method newBrowserWin () = - let win = new browserWin () in - win#check_widgets (); - win + object (self) + inherit browserWin () + val combo = GEdit.combo_box_entry () + initializer + self#check_widgets (); + let combo_widget = combo#coerce in + uriHBox#add combo_widget + method browserUri = combo + end method newUriDialog () = let dialog = new uriChoiceDialog () in @@ -310,9 +363,12 @@ let is_var_uri s = String.sub s (String.length s - 4) 4 = ".var" with Invalid_argument _ -> false +(* this is a shit and should be changed :-{ *) let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") - ?(msg = "") ?(nonvars_button = false) () + ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) + ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) + ?copy_cb () ~id uris = let gui = instance () in @@ -323,11 +379,28 @@ let interactive_uri_choice Lazy.force nonvars_uris else begin let dialog = gui#newUriDialog () in + if hide_uri_entry then + dialog#uriEntryHBox#misc#hide (); + if hide_try then + begin + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + end; + dialog#okLabel#set_label ok_label; dialog#uriChoiceTreeView#selection#set_mode (selection_mode :> Gtk.Tags.selection_mode); let model = new stringListModel dialog#uriChoiceTreeView in let choices = ref None in let nonvars = ref false in + (match copy_cb with + | None -> () + | Some cb -> + dialog#copyButton#misc#show (); + connect_button dialog#copyButton + (fun _ -> + match model#easy_selection () with + | [u] -> (cb u) + | _ -> ())); dialog#uriChoiceDialog#set_title title; dialog#uriChoiceLabel#set_text msg; List.iter model#easy_append uris; @@ -340,9 +413,15 @@ let interactive_uri_choice ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); connect_button dialog#uriChoiceConstantsButton (fun _ -> return (Some (Lazy.force nonvars_uris))); - connect_button dialog#uriChoiceAutoButton (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some (Lazy.force nonvars_uris))); + if ok_action = `AUTO then + connect_button dialog#uriChoiceAutoButton (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" true; + return (Some (Lazy.force nonvars_uris))) + else + connect_button dialog#uriChoiceAutoButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); connect_button dialog#uriChoiceSelectedButton (fun _ -> match model#easy_selection () with | [] -> ()