X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=55b044ba44662b286493d077229d9ced6b82955c;hb=6b61a9e6698a7c1936adf217b599e34e65a5e4c9;hp=3ba6499a93acab767646871f0559dcd6ff848576;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 3ba6499a9..55b044ba4 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -428,9 +428,10 @@ class gui () = ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png")) ~name:"Matita" ~version:BuildTimeConf.version - ~website:"http://helm.cs.unibo.it" + ~website:"http://matita.cs.unibo.it" () in + ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ())); connect_menu_item main#contentsMenuItem (fun () -> let cmd = sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir @@ -904,6 +905,33 @@ class gui () = c#load (`About `Coercions)); connect_menu_item main#showAutoGuiMenuItem (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); + connect_menu_item main#showTermGrammarMenuItem + (fun _ -> + let w = GWindow.window ~resizable:true + ~position:`CENTER_ON_PARENT + ~title:"Terms grammar" ~width:640 ~height:400 () in + w#set_transient_for (main#toplevel#as_window); + let s = GBin.scrolled_window () in + (w :> GContainer.container)#add (s :> GObj.widget); + let t = GText.view () in + t#buffer#insert (Print_grammar.ebnf_of_term ()); + s#add (t:>GObj.widget); + w#show ()); + connect_menu_item main#showUnicodeTable + (fun _ -> + let w = GWindow.window ~resizable:true + ~position:`CENTER_ON_PARENT + ~title:"Tex/UTF8 table" ~width:640 ~height:400 () in + w#set_transient_for (main#toplevel#as_window); + let s = GBin.scrolled_window () in + (w :> GContainer.container)#add (s :> GObj.widget); + let t = GTree.view () in + let m = new MatitaGtkMisc.multiStringListModel ~cols:2 t in + List.iter (fun (k,vs) -> + m#easy_mappend [k;String.concat " " vs]) + (Utf8Macro.pp_table ()); + s#add (t:>GObj.widget); + w#show ()); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *)