File: gtk_ext.ml

package info (click to toggle)
prooftree 0.13-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid, stretch
  • size: 592 kB
  • ctags: 668
  • sloc: ml: 4,462; sh: 117; makefile: 111
file content (144 lines) | stat: -rw-r--r-- 4,884 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
(* 
 * prooftree --- proof tree display for Proof General
 * 
 * Copyright (C) 2011 - 2016 Hendrik Tews
 * 
 * This file is part of "prooftree".
 * 
 * "prooftree" is free software: you can redistribute it and/or
 * modify it under the terms of the GNU General Public License as
 * published by the Free Software Foundation, either version 3 of the
 * License, or (at your option) any later version.
 * 
 * "prooftree" is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 * General Public License in file COPYING in this or one of the parent
 * directories for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with "prooftree". If not, see <http://www.gnu.org/licenses/>.
 * 
 * $Id: gtk_ext.ml,v 1.19 2016/01/23 12:57:14 tews Exp $
 *)


(** Some misc LablGtk extensions *)


(** An extension of {xref lablgtk class GDraw.drawable} with a few
    convinience methods. 
*)
class better_drawable ?colormap w pc = 
object
  inherit GDraw.drawable ?colormap w

  (** Link a writable Pango context for easy access. *)
  val pango_context = (pc : GPango.context_rw)

  (** Return a writable Pango context. *)
  method pango_context = pango_context    

  (** Return the current foreground color of the graphics context of
      this drawable. 
  *)
  method get_foreground = (Gdk.GC.get_values gc).Gdk.GC.foreground

  (** Return the current background color of the graphics context of
      this drawable. 
  *)
  method get_background = (Gdk.GC.get_values gc).Gdk.GC.background
end


(** Convinience wrapper around {xref lablgtk val
    GWindow.message_dialog}. [run_message_dialog message message_type]
    displays a modal message dialog of [message_type] with message
    [message] and one OK button. The dialog is destroyed when the OK
    button is pressed. [message_type] must be one of [`INFO],
    [`WARNING], [`QUESTION] and [`ERROR ].
*)
let run_message_dialog message message_type =
  let warn = GWindow.message_dialog ~message ~message_type
    ~buttons:GWindow.Buttons.ok ()
  in
  ignore(warn#run());
  warn#destroy()


(** Another convenience wrapper around {xref lablgtk val
    GWindow.message_dialog}. [error_message_dialog message] displays a
    modal error message dialog (of type [`ERROR]) with message
    [message] and one OK button. The application is terminated with
    exit status 1 after the error has been acknowledged.
*)
let error_message_dialog message =
  run_message_dialog message `ERROR;
  exit 1


(** Scroll the given adjustment [direction] number of pages into the
    direction idicated by the sign of [direction]. This function is
    used for scrolling with keys.
*)
let scroll_adjustment (a : GData.adjustment) direction =
  let new_val = a#value +. float_of_int(direction) *. a#step_increment in
  let new_val = if new_val < 0.0 then 0.0 else new_val in
  let max = max 0.0 (a#upper -. a#page_size) in
  let new_val = if new_val > max then max else new_val in
  a#set_value new_val


(** [inside_adj_range adjustment x] checks if [x] is inside the
    visible range of the adjustment [adjustment].
*)
let inside_adj_range adjustment x =
  let page_l = adjustment#value in
  let page_u = page_l +. adjustment#page_size in
  page_l <= x && x <= page_u

(** [range_inside_adj_range adjustment xl xh] checks if the range from
    [xl] to [xh] is inside the visible range of the adjustment
    [adjustment]. Does only produce correct results if [xl <= xh].
*)
let range_inside_adj_range adjustment xl xh =
  let page_l = adjustment#value in
  let page_u = page_l +. adjustment#page_size in
  page_l <= xl && xh <= page_u



(** Round a 16-bit color value to 8 bit. *)
let round_color_2_digits co =
  min ((co + 128) / 256) 0xff


(** [pango_markup_color s color] adds Pango markup for using color
    [color] arouns [s].
*)
let pango_markup_color s color =
  Printf.sprintf
    "<span color=\"#%02X%02X%02X\">%s</span>"
    (round_color_2_digits (Gdk.Color.red color))
    (round_color_2_digits (Gdk.Color.green color))
    (round_color_2_digits (Gdk.Color.blue color))
    s

(** [pango_markup_bold_color s color] adds Pango markup for using a
    bold font in color [color] arouns [s].
*)
let pango_markup_bold_color s color =
  Printf.sprintf
    "<span weight=\"bold\" color=\"#%02X%02X%02X\">%s</span>"
    (round_color_2_digits (Gdk.Color.red color))
    (round_color_2_digits (Gdk.Color.green color))
    (round_color_2_digits (Gdk.Color.blue color))
    s

(* XXX why is this necessary?? *)
(** Reallocate a Gdk color. This is necessary because some operations
    copy only the RGB values of a color, leaving the internal color
    field uninitialized.
*)
let realloc_color c =
  GDraw.color (`RGB((Gdk.Color.red c), (Gdk.Color.green c),(Gdk.Color.blue c)))