- let gui = instance () in
- let dialog = gui#newUriDialog () in
- dialog#uriEntryHBox#misc#hide ();
- dialog#uriChoiceSelectedButton#misc#hide ();
- dialog#uriChoiceAutoButton#misc#hide ();
- dialog#uriChoiceConstantsButton#misc#hide ();
- dialog#uriChoiceTreeView#selection#set_mode
- (`SINGLE :> Gtk.Tags.selection_mode);
- let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
- dialog#uriChoiceDialog#set_title title;
- let hack_len = MatitaGtkMisc.utf8_string_length text in
- let rec colorize acc_len = function
- | [] ->
- let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
- 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
- escape_pango_markup str1 ^ "<b>" ^
- escape_pango_markup str2 ^ "</b>" ^
- colorize stop tl
- in
+ let dialog = new uriChoiceDialog () in
+ dialog#uriEntryHBox#misc#hide ();
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceAutoButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ dialog#uriChoiceTreeView#selection#set_mode
+ (`SINGLE :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ dialog#uriChoiceDialog#set_title title;
+ let hack_len = MatitaGtkMisc.utf8_string_length text in
+ let rec colorize acc_len = function
+ | [] ->
+ let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
+ 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
+ escape_pango_markup str1 ^ "<b>" ^
+ escape_pango_markup str2 ^ "</b>" ^
+ colorize stop tl
+ in