Semantic analysis implemented (sort of).

[helm.git] / helm / software / matita / matitaGui.ml

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 98612ab2bf1f7b12b426fe8ea4a10694c6cbec0b..55b044ba44662b286493d077229d9ced6b82955c 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -905,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 *)