X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=50d3f8ce8b046b9d338deb77f68af70462cc7f5d;hb=bd6f44797ad9d5b72e2177d885f5e56aaa2bea4d;hp=ec4d042ff38223eb61cd6151c84b7f19171c8d99;hpb=716da638633f01d6a5b52c05e0bd6adc86385b60;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index ec4d042ff..50d3f8ce8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -63,7 +63,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 +156,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."); + 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."); 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,6 +225,17 @@ 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 = Pango.Font.from_string "Monospace 10" in + let monospace_tag = + self#main#scriptTextView#buffer#create_tag [`FONT_DESC font] + in + 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 *) @@ -227,7 +243,27 @@ class gui () = self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png"; self#main#hintHighImage#set_file "icons/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 @@ -310,9 +346,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 +362,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 +396,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 | [] -> ()