let toggle_callback ~callback ~(check: GMenu.check_menu_item) =
ignore (check#connect#toggled (fun _ -> callback check#active))
-let add_key_binding key callback (evbox: GBin.event_box) =
- ignore (evbox#event#connect#key_press (function
- | key' when GdkEvent.Key.keyval key' = key ->
- callback ();
- false
- | _ -> false))
-
class multiStringListModel ~cols (tree_view: GTree.view) =
let column_list = new GTree.column_list in
let text_columns =
let popup_message
~title ~message ~buttons ~callback
?(message_type=`QUESTION) ?parent ?(use_markup=true)
- ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false)
- ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
- ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width
+ ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false)
+ ?screen ?type_hint
+ ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width
?height ?(show=true) ()
=
let m =
GWindow.message_dialog
~message ~use_markup ~message_type ~buttons ?parent ~destroy_with_parent
- ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen
- ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height
+ ~title ?icon ~modal ~resizable ?screen
+ ?type_hint ~position ?wmclass ?border_width ?width ?height
~show ()
in
ignore(m#connect#response
let popup_message_lowlevel
~title ~message ?(no_separator=true) ~callback ~message_type ~buttons
- ?parent ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false)
+ ?parent ?(destroy_with_parent=true)
?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
- ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width
+ ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width
?height ?(show=true) ()
=
let m =
GWindow.dialog
~no_separator
?parent ~destroy_with_parent
- ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen
- ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height
+ ~title ?icon ~modal ~resizable ?screen
+ ?type_hint ~position ?wmclass ?border_width ?width ?height
~show:false ()
in
let stock =
text
;;
-
+let matita_lang =
+ let source_language_manager =
+ GSourceView3.source_language_manager ~default:true in
+ source_language_manager#set_search_path
+ (BuildTimeConf.runtime_base_dir ::
+ source_language_manager#search_path);
+ match source_language_manager#language "grafite" with
+ | None ->
+ HLog.error(sprintf "can't load a language file for \"grafite\" in %s"
+ BuildTimeConf.runtime_base_dir);
+ assert false
+ | Some x -> x
+;;