X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=c6510403521af1e3cb8a70ba0a6a4ab0cc98ad1c;hb=6d297b12c480352eb2f156ab4515f73921ea2e81;hp=c1f9a992a37eb43c005feecfebf0a9aa99f38e48;hpb=f4117d09d2bdba02657ed83ab98cfae8c90cf8d2;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index c1f9a992a..c65104035 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -42,7 +42,7 @@ class type browserWin =
    * lablgladecc :-(((( *)
 object
   inherit MatitaGeneratedGui.browserWin
-  method browserUri: GEdit.combo_box_entry
+  method browserUri: GEdit.entry
 end
 
 class console ~(buffer: GText.buffer) () =
@@ -907,18 +907,12 @@ class gui () =
         (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
       connect_menu_item main#showTermGrammarMenuItem 
         (fun _ -> 
-           let w = MatitaGtkMisc.new_search_win "Terms grammar" (Print_grammar.ebnf_of_term ()) in
-           w#toplevel#set_transient_for (main#toplevel#as_window);
-           w#toplevel#show ());
+          let c = MatitaMathView.cicBrowser () in
+          c#load (`About `Grammar));
       connect_menu_item main#showUnicodeTable
         (fun _ -> 
-           let text = String.concat "\n"
-            (List.map (fun (k,vs) -> k ^ "\t" ^ String.concat ",  " vs)
-             (Utf8Macro.pp_table ())) 
-           in
-           let w = MatitaGtkMisc.new_search_win "TeX/UTF8 table" text in
-           w#toplevel#set_transient_for (main#toplevel#as_window);
-           w#toplevel#show ());
+          let c = MatitaMathView.cicBrowser () in
+          c#load (`About `TeX));
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)
@@ -968,7 +962,7 @@ class gui () =
            end));
       (* math view handling *)
       connect_menu_item main#newCicBrowserMenuItem (fun () ->
-        ignore (MatitaMathView.cicBrowser ()));
+        ignore(MatitaMathView.cicBrowser ()));
       connect_menu_item main#increaseFontSizeMenuItem (fun () ->
         self#increaseFontSize ();
         MatitaMathView.increase_font_size ();
@@ -1167,12 +1161,12 @@ class gui () =
     method newBrowserWin () =
       object (self)
         inherit browserWin ()
-        val combo = GEdit.combo_box_entry ()
+        val combo = GEdit.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 ()
+          combo#misc#grab_focus ()
         method browserUri = combo
       end
 
@@ -1237,7 +1231,8 @@ class gui () =
 
     method private updateFontSize () =
       self#sourceView#misc#modify_font_by_name
-        (sprintf "%s %d" BuildTimeConf.script_font font_size)
+        (sprintf "%s %d" BuildTimeConf.script_font font_size);
+      MatitaAutoGui.set_font_size font_size
 
     method increaseFontSize () =
       font_size <- font_size + 1;
@@ -1381,9 +1376,10 @@ class interpModel =
         tree_store#get ~row:iter ~column:interp_no_col
     end
 
+
 let interactive_string_choice 
   text prefix_len ?(title = "") ?(msg = "") () ~id locs uris 
-=
+= 
   let gui = instance () in
     let dialog = gui#newUriDialog () in
     dialog#uriEntryHBox#misc#hide ();
@@ -1399,13 +1395,15 @@ let interactive_string_choice
     let rec colorize acc_len = function
       | [] -> 
           let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
-          fst(MatitaGtkMisc.utf8_parsed_text text floc)
+          escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
       | he::tl -> 
           let start, stop =  HExtlib.loc_of_floc he in
           let floc1 = HExtlib.floc_of_loc (acc_len,start) in
           let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
           let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
-          str1 ^ "<b>" ^ str2 ^ "</b>" ^ colorize stop tl
+          escape_pango_markup str1 ^ "<b>" ^ 
+          escape_pango_markup str2 ^ "</b>" ^ 
+          colorize stop tl
     in
 (*     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
                 Printf.eprintf "(%d,%d)" start stop) locs; *)
@@ -1424,6 +1422,7 @@ let interactive_string_choice
     let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
       (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
     in
+  prerr_endline ("txt:" ^ txt);
     dialog#uriChoiceLabel#set_label txt;
     List.iter model#easy_append uris;
     let return v =