aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-05-06 13:41:03 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-05-06 13:41:03 +0000
commit67df75285764fd0d192675cfcd3999936864d90a (patch)
tree38ccc56c0814eafcfcdb530737d3acae1d3b3066 /ide/coqide.ml
parent9fa14555270fa8f2368a7f4df1510bd2937d25ec (diff)
Coqide: view -> zoom in / out / fit
This commit adds zoom facilities that are useful for demos (quickly increate font size) and daily use (set size so that 80 colums fit the window width). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml26
1 files changed, 26 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2f52e5a48..8cca8eb9a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -965,6 +965,32 @@ let build_ui () =
item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right"
~stock:`GO_FORWARD
~callback:(fun _ -> notebook#next_page ());
+ item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus")
+ ~stock:`ZOOM_IN ~callback:(fun _ ->
+ Pango.Font.set_size current.text_font
+ (Pango.Font.get_size current.text_font + Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ());
+ item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
+ ~stock:`ZOOM_OUT ~callback:(fun _ ->
+ Pango.Font.set_size current.text_font
+ (Pango.Font.get_size current.text_font - Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ());
+ item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
+ ~stock:`ZOOM_FIT ~callback:(fun _ ->
+ let script = notebook#current_term.script in
+ let space = script#misc#allocation.Gtk.width in
+ let cols = script#right_margin_position in
+ let pango_ctx = script#misc#pango_context in
+ let layout = pango_ctx#create_layout in
+ let fsize = Pango.Font.get_size current.text_font in
+ Pango.Layout.set_text layout (String.make cols 'X');
+ let tlen = fst (Pango.Layout.get_pixel_size layout) in
+ Pango.Font.set_size current.text_font
+ (fsize * space / tlen / Pango.scale * Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ());
toggle_item "Show Toolbar" ~label:"Show _Toolbar"
~active:(prefs.show_toolbar)
~callback:(fun _ ->