X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=8eec3244d29915ff57768b0acb1f0de7961c2cc4;hb=842919f2f8ee71a5301ad962220569450340a9e9;hp=5045f36d1aa5148bd3ec80c2f3c3a7fa4b46ed26;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5045f36d1..8eec3244d 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" ] @@ -60,10 +68,25 @@ class gui () = [ main#mainWinEventBox ] in let console = new console ~buffer:main#logTextView#buffer () in + let (source_view: GSourceView.source_view) = + GSourceView.source_view + ~auto_indent:true + ~insert_spaces_instead_of_tabs:true ~tabs_width:2 + ~margin:80 ~show_margin:true + ~smart_home_end:true + ~packing:main#scriptScrolledWin#add + () + in + let default_font_size = + Helm_registry.get_opt_default Helm_registry.int + ~default:BuildTimeConf.default_font_size "matita.font_size" + in + let source_buffer = source_view#source_buffer in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false - val mutable script_fname = None + val mutable script_fname = None + val mutable font_size = default_font_size initializer (* glade's check widgets *) @@ -125,7 +148,7 @@ class gui () = in let tac_w_term ast _ = if (MatitaScript.instance ())#onGoingProof () then - let (buf: GText.buffer) = self#main#scriptTextView#buffer in + let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ TacticAstPp.pp_tactic ast) in @@ -145,7 +168,21 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,None,None))); + MatitaGtkMisc.toggle_widget_visibility + ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) + ~check:self#main#tacticsBarMenuItem; + let module Hr = Helm_registry in + if + not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") + then + self#main#tacticsBarMenuItem#set_active false; + MatitaGtkMisc.toggle_callback + ~callback:(function + | true -> self#main#toplevel#fullscreen () + | false -> self#main#toplevel#unfullscreen ()) + ~check:self#main#fullscreenMenuItem; + self#main#fullscreenMenuItem#set_active false; (* quit *) self#setQuitCallback (fun () -> exit 0); (* log *) @@ -155,6 +192,15 @@ class gui () = MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))); (* script *) + let _ = + match GSourceView.source_language_from_file BuildTimeConf.lang_file with + | None -> + MatitaLog.warn (sprintf "can't load language file %s" + BuildTimeConf.lang_file) + | Some matita_lang -> + source_buffer#set_language matita_lang; + source_buffer#set_highlight true + in let s () = MatitaScript.instance () in let disableSave () = script_fname <- None; @@ -166,7 +212,7 @@ class gui () = | Some f -> script#reset (); script#loadFrom f; - console#message ("'"^f^"' loaded."); + console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f | None -> () in @@ -175,7 +221,7 @@ class gui () = match self#chooseFile ~ok_not_exists:true () with | Some f -> script#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); self#_enableSaveTo f | None -> () in @@ -184,12 +230,12 @@ class gui () = | None -> saveAsScript () | Some f -> (s ())#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); 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")) + source_buffer#place_cursor + (source_buffer#get_iter_at_mark (`NAME "locked")) in let advance _ = (MatitaScript.instance ())#advance (); cursor () in let retract _ = (MatitaScript.instance ())#retract (); cursor () in @@ -199,7 +245,7 @@ class gui () = let connect_key sym f = connect_key self#main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; - connect_key self#main#scriptTextView#event + connect_key self#sourceView#event ~modifiers:[`CONTROL] ~stop:true sym f in connect_button self#main#scriptAdvanceButton advance; @@ -217,22 +263,32 @@ class gui () = connect_menu_item self#main#newMenuItem newScript; connect_key GdkKeysyms._period (fun () -> - let buf = self#main#scriptTextView#buffer in - buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n"; - advance ()); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + ".\n"; + advance ()); connect_key GdkKeysyms._Return (fun () -> - let buf = self#main#scriptTextView#buffer in - buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n"; - advance ()); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + "\n"; + advance ()); + (* script monospace font stuff *) + self#updateFontSize (); (* 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#sourceView#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 * 6 / 10 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 @@ -247,39 +303,22 @@ class gui () = method console = console - + method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) method about = about method fileSel = fileSel method main = main method newBrowserWin () = - let win = new browserWin () in - win#whelpImage2#set_file "icons/whelp.png"; - win#whelpBarToggleButton#set_active false; - win#whelpBarBox#misc#hide (); - win#mathOrListNotebook#set_show_tabs false; - connect_toggle_button win#whelpBarToggleButton - (fun () -> - if win#whelpBarToggleButton#active then - win#whelpBarBox#misc#show () - else - win#whelpBarBox#misc#hide ()); - let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in - let combo,(combo_store,combo_column) = - GEdit.combo_box_text ~strings:queries () - in - combo#set_active 0; - win#comboVbox#add (combo :> GObj.widget); - let start_query () = - let query = String.lowercase (List.nth queries combo#active) in - let input = win#queryInputText#text in - let statement = "whelp " ^ query ^ " " ^ input ^ "." in - (MatitaScript.instance ())#advance ~statement () - in - ignore(win#queryInputText#connect#activate ~callback:start_query); - ignore(combo#connect#changed ~callback:start_query); - 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#pack ~from:`END ~fill:true ~expand:true combo_widget; + combo#entry#misc#grab_focus () + method browserUri = combo + end method newUriDialog () = let dialog = new uriChoiceDialog () in @@ -335,6 +374,22 @@ class gui () = GtkThread.main (); !text + method private updateFontSize () = + self#sourceView#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font font_size) + + method increaseFontSize () = + font_size <- font_size + 1; + self#updateFontSize () + + method decreaseFontSize () = + font_size <- font_size - 1; + self#updateFontSize () + + method resetFontSize () = + font_size <- default_font_size; + self#updateFontSize () + end let gui () = @@ -346,19 +401,16 @@ let instance = singleton gui let non p x = not (p x) -let is_var_uri s = - try - 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) ?(hide_uri_entry=false) - ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb () + ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) + ?copy_cb () ~id uris = let gui = instance () in - let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in + let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in if (selection_mode <> `SINGLE) && (Helm_registry.get_bool "matita.auto_disambiguation") then @@ -389,7 +441,7 @@ let interactive_uri_choice | _ -> ())); dialog#uriChoiceDialog#set_title title; dialog#uriChoiceLabel#set_text msg; - List.iter model#easy_append uris; + List.iter model#easy_append (List.map UriManager.string_of_uri uris); dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; let return v = choices := v; @@ -399,13 +451,19 @@ 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 (List.map UriManager.uri_of_string uris))); connect_button dialog#uriChoiceSelectedButton (fun _ -> match model#easy_selection () with | [] -> () - | uris -> return (Some uris)); + | uris -> return (Some (List.map UriManager.uri_of_string uris))); connect_button dialog#uriChoiceAbortButton (fun _ -> return None); dialog#uriChoiceDialog#show (); GtkThread.main ();