The Birdfont Source Code


All Repositories / birdfont.git / blob – RSS feed

OverView.vala in libbirdfont

This file is a part of the Birdfont project.

Contributing

Send patches or pull requests to johan.mattsson.m@gmail.com.
Clone this repository: git clone https://github.com/johanmattssonm/birdfont.git

Revisions

View the latest version of libbirdfont/OverView.vala.
Store zoom value
1 /* 2 Copyright (C) 2012 - 2016 Johan Mattsson 3 4 This library is free software; you can redistribute it and/or modify 5 it under the terms of the GNU Lesser General Public License as 6 published by the Free Software Foundation; either version 3 of the 7 License, or (at your option) any later version. 8 9 This library is distributed in the hope that it will be useful, but 10 WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 12 Lesser General Public License for more details. 13 */ 14 15 using Cairo; 16 17 namespace BirdFont { 18 19 /** A display with all glyphs present in this font. */ 20 public class OverView : FontDisplay { 21 public WidgetAllocation allocation = new WidgetAllocation (); 22 23 public OverViewItem selected_item = new OverViewItem (); 24 25 public Gee.ArrayList<GlyphCollection> copied_glyphs = new Gee.ArrayList<GlyphCollection> (); 26 public Gee.ArrayList<GlyphCollection> selected_items = new Gee.ArrayList<GlyphCollection> (); 27 28 int selected = 0; 29 int first_visible = 0; 30 int rows = 0; 31 int items_per_row = 0; 32 33 double view_offset_y = 0; 34 double view_offset_x = 0; 35 36 public signal void open_new_glyph_signal (unichar c); 37 public signal void open_glyph_signal (GlyphCollection c); 38 39 public GlyphRange glyph_range { 40 get { 41 return _glyph_range; 42 } 43 44 set { 45 _glyph_range = value; 46 } 47 } 48 49 GlyphRange _glyph_range; 50 51 string search_query = ""; 52 53 public Gee.ArrayList<OverViewItem> visible_items = new Gee.ArrayList<OverViewItem> (); 54 55 /** List of undo commands. */ 56 public Gee.ArrayList<OverViewUndoItem> undo_items = new Gee.ArrayList<OverViewUndoItem> (); 57 public Gee.ArrayList<OverViewUndoItem> redo_items = new Gee.ArrayList<OverViewUndoItem> (); 58 59 /** Show all characters that has been drawn. */ 60 public bool all_available { 61 set { 62 _all_available = value; 63 update_item_list (); 64 } 65 66 get { 67 return _all_available; 68 } 69 } 70 71 bool _all_available = false; 72 73 /** Show unicode database info. */ 74 CharacterInfo? character_info = null; 75 76 double scroll_size = 1; 77 const double UCD_LINE_HEIGHT = 17 * 1.3; 78 79 private bool update_scheduled = true; 80 81 public OverView (GlyphRange? range = null, 82 bool open_selected = true, bool default_character_set = true) { 83 84 GlyphRange gr; 85 86 if (range == null) { 87 gr = new GlyphRange (); 88 set_current_glyph_range (gr); 89 } 90 91 if (open_selected) { 92 this.open_glyph_signal.connect ((glyph_collection) => { 93 TabBar tabs = MainWindow.get_tab_bar (); 94 string n = glyph_collection.get_current ().name; 95 bool selected = tabs.select_char (n); 96 Glyph g = glyph_collection.get_current (); 97 GlyphTab glyph_tab; 98 99 if (!selected) { 100 glyph_tab = new GlyphTab (glyph_collection); 101 tabs.add_tab (glyph_tab, true, glyph_collection); 102 set_glyph_zoom (glyph_collection); 103 PenTool.update_orientation (); 104 } 105 }); 106 107 this.open_new_glyph_signal.connect ((character) => { 108 // ignore control characters 109 if (character <= 0x1F) { 110 return; 111 } 112 113 create_new_glyph (character); 114 }); 115 } 116 117 if (default_character_set) { 118 IdleSource idle = new IdleSource (); 119 120 idle.set_callback (() => { 121 use_default_character_set (); 122 selected_canvas (); 123 return false; 124 }); 125 126 idle.attach (null); 127 } 128 129 update_item_list (); 130 update_scrollbar (); 131 reset_zoom (); 132 133 string? zoom = Preferences.get ("overview_zoom"); 134 135 if (zoom != null) { 136 string z = (!) zoom; 137 138 if (z != "") { 139 set_zoom (double.parse (z)); 140 } 141 } 142 } 143 144 public Glyph? get_selected_glyph () { 145 if (selected_items.size == 0) { 146 return null; 147 } 148 149 return selected_items.get (0).get_current (); 150 } 151 152 public void select_all_glyphs () { 153 Font f; 154 GlyphCollection? glyphs; 155 156 f = BirdFont.get_current_font (); 157 158 for (int index = 0; index < f.length (); index++) { 159 glyphs = f.get_glyph_collection_index ((uint32) index); 160 return_if_fail (glyphs != null); 161 162 selected_items.add ((!) glyphs); 163 } 164 165 foreach (OverViewItem item in visible_items) { 166 item.selected = item.glyphs != null; 167 } 168 169 GlyphCanvas.redraw (); 170 } 171 172 public void use_default_character_set () { 173 GlyphRange gr = new GlyphRange (); 174 all_available = false; 175 DefaultCharacterSet.use_default_range (gr); 176 set_current_glyph_range (gr); 177 OverviewTools.update_overview_characterset (); 178 FontDisplay.dirty_scrollbar = true; 179 } 180 181 public GlyphCollection create_new_glyph (unichar character) { 182 StringBuilder name = new StringBuilder (); 183 TabBar tabs = MainWindow.get_tab_bar (); 184 bool selected; 185 Glyph glyph; 186 GlyphCollection glyph_collection; 187 GlyphCanvas canvas; 188 GlyphTab glyph_tab; 189 190 glyph_collection = MainWindow.get_current_glyph_collection (); 191 name.append_unichar (character); 192 selected = tabs.select_char (name.str); 193 194 if (!selected) { 195 glyph_collection = add_character_to_font (character); 196 glyph_tab = new GlyphTab (glyph_collection); 197 glyph = glyph_collection.get_current (); 198 glyph.layers.add_layer (new Layer ()); 199 tabs.add_tab (glyph_tab, true, glyph_collection); 200 201 selected_items.add (glyph_collection); 202 203 canvas = MainWindow.get_glyph_canvas (); 204 canvas.set_current_glyph_collection (glyph_collection); 205 206 set_glyph_zoom (glyph_collection); 207 } else { 208 warning ("Glyph is already open"); 209 } 210 211 OverviewTools.update_overview_characterset (); 212 return glyph_collection; 213 } 214 215 public GlyphCollection add_empty_character_to_font (unichar character, bool unassigned, string name) { 216 return add_character_to_font (character, true, unassigned); 217 } 218 219 public GlyphCollection add_character_to_font (unichar character, bool empty = false, 220 bool unassigned = false, string glyph_name = "") { 221 StringBuilder name = new StringBuilder (); 222 Font font = BirdFont.get_current_font (); 223 GlyphCollection? fg; 224 Glyph glyph; 225 GlyphCollection glyph_collection; 226 227 if (glyph_name == "") { 228 name.append_unichar (character); 229 } else { 230 name.append (glyph_name); 231 } 232 233 if (all_available) { 234 fg = font.get_glyph_collection_by_name (name.str); 235 } else { 236 fg = font.get_glyph_collection (name.str); 237 } 238 239 if (fg != null) { 240 glyph_collection = (!) fg; 241 } else { 242 glyph_collection = new GlyphCollection (character, name.str); 243 244 if (!empty) { 245 glyph = new Glyph (name.str, !unassigned ? character : '\0'); 246 glyph_collection.add_master (new GlyphMaster ()); 247 glyph_collection.insert_glyph (glyph, true); 248 } 249 250 font.add_glyph_collection (glyph_collection); 251 } 252 253 glyph_collection.set_unassigned (unassigned); 254 255 return glyph_collection; 256 } 257 258 public static void search () { 259 OverView ow = MainWindow.get_overview (); 260 TextListener listener = new TextListener (t_("Search"), ow.search_query, t_("Filter")); 261 262 listener.signal_text_input.connect ((text) => { 263 OverView o = MainWindow.get_overview (); 264 o.search_query = text; 265 }); 266 267 listener.signal_submit.connect (() => { 268 OverView o = MainWindow.get_overview (); 269 string q = o.search_query; 270 271 if (q.char_count () > 1) { 272 q = q.down (); 273 } 274 275 GlyphRange r = CharDatabase.search (q); 276 o.set_current_glyph_range (r); 277 MainWindow.get_tab_bar ().select_tab_name ("Overview"); 278 279 TextListener tl = new TextListener (t_("Search"), o.search_query, t_("Filter")); 280 TabContent.show_text_input (tl); 281 }); 282 283 TabContent.show_text_input (listener); 284 } 285 286 public Glyph? get_current_glyph () { 287 OverViewItem oi = selected_item; 288 if (oi.glyphs != null) { 289 return ((!) oi.glyphs).get_current (); 290 } 291 return null; 292 } 293 294 public void set_glyph_zoom (GlyphCollection glyphs) { 295 GlyphCanvas canvas; 296 canvas = MainWindow.get_glyph_canvas (); 297 canvas.set_current_glyph_collection (glyphs); 298 Toolbox tools = MainWindow.get_toolbox (); 299 ZoomTool z = (ZoomTool) tools.get_tool ("zoom_tool"); 300 z.store_current_view (); 301 glyphs.get_current ().default_zoom (); 302 z.store_current_view (); 303 OverViewItem.reset_label (); 304 } 305 306 public double get_height () { 307 double l; 308 Font f; 309 310 if (rows == 0) { 311 return 0; 312 } 313 314 if (all_available) { 315 f = BirdFont.get_current_font (); 316 l = f.length (); 317 } else { 318 l = glyph_range.length (); 319 } 320 321 return 2.0 * OverViewItem.height * (l / rows); 322 } 323 324 public bool selected_char_is_visible () { 325 return first_visible <= selected <= first_visible + items_per_row * rows; 326 } 327 328 public override bool has_scrollbar () { 329 return true; 330 } 331 332 public bool all_characters_in_view () { 333 double length; 334 Font f; 335 336 if (all_available) { 337 f = BirdFont.get_current_font (); 338 length = f.length (); 339 } else { 340 length = glyph_range.length (); 341 } 342 343 return length < items_per_row * rows; 344 } 345 346 public void move_up () { 347 first_visible -= items_per_row; 348 selected += items_per_row; 349 350 if (first_visible < 0) { 351 selected -= items_per_row; 352 first_visible = 0; 353 view_offset_y = 0; 354 } 355 } 356 357 public void move_down () { 358 if (!at_bottom ()) { 359 first_visible += items_per_row; 360 selected -= items_per_row; 361 } 362 } 363 364 public override void scroll_wheel (double x, double y, double dx, double dy) { 365 double pixel_delta = 3 * dy; 366 367 if (dy > 0) { 368 view_offset_y += pixel_delta; 369 370 while (view_offset_y > 0) { 371 view_offset_y -= OverViewItem.height; 372 move_up (); 373 } 374 } else { 375 if (at_bottom ()) { 376 if (view_offset_y > -2 * OverViewItem.height && !all_characters_in_view ()) { 377 view_offset_y += pixel_delta; 378 } 379 } else { 380 view_offset_y += pixel_delta; 381 while (view_offset_y < -OverViewItem.height) { 382 view_offset_y += OverViewItem.height; 383 move_down (); 384 } 385 } 386 } 387 388 if (view_offset_y < -2 * OverViewItem.height) { 389 view_offset_y = -2 * OverViewItem.height; 390 } 391 392 update_item_list (); 393 update_scrollbar (); 394 hide_menu (); 395 GlyphCanvas.redraw (); 396 } 397 398 public override void selected_canvas () { 399 OverviewTools.update_overview_characterset (); 400 KeyBindings.set_require_modifier (true); 401 update_scrollbar (); 402 update_zoom_bar (); 403 OverViewItem.glyph_scale = 1; 404 update_item_list (); 405 selected_item = get_selected_item (); 406 GlyphCanvas.redraw (); 407 } 408 409 public void update_zoom_bar () { 410 double z = OverViewItem.width / OverViewItem.DEFAULT_WIDTH - 0.5; 411 Toolbox.overview_tools.zoom_bar.set_zoom (z); 412 Toolbox.redraw_tool_box (); 413 update_item_list (); 414 } 415 416 public void set_zoom (double zoom) { 417 double z = zoom + 0.5; 418 OverViewItem.glyph_scale = 1; 419 OverViewItem.width = OverViewItem.DEFAULT_WIDTH * z; 420 OverViewItem.height = OverViewItem.DEFAULT_HEIGHT * z; 421 OverViewItem.margin = OverViewItem.DEFAULT_MARGIN * z; 422 update_item_list (); 423 OverViewItem.reset_label (); 424 GlyphCanvas.redraw (); 425 Preferences.set ("overview_zoom", @"$zoom"); 426 } 427 428 public override void zoom_min () { 429 OverViewItem.width = OverViewItem.DEFAULT_WIDTH * 0.5; 430 OverViewItem.height = OverViewItem.DEFAULT_HEIGHT * 0.5; 431 OverViewItem.margin = OverViewItem.DEFAULT_MARGIN * 0.5; 432 update_item_list (); 433 OverViewItem.reset_label (); 434 GlyphCanvas.redraw (); 435 update_zoom_bar (); 436 } 437 438 public override void reset_zoom () { 439 OverViewItem.width = OverViewItem.DEFAULT_WIDTH; 440 OverViewItem.height = OverViewItem.DEFAULT_HEIGHT; 441 OverViewItem.margin = OverViewItem.DEFAULT_MARGIN; 442 update_item_list (); 443 OverViewItem.reset_label (); 444 GlyphCanvas.redraw (); 445 update_zoom_bar (); 446 } 447 448 public override void zoom_max () { 449 OverViewItem.width = allocation.width; 450 OverViewItem.height = allocation.height; 451 update_item_list (); 452 OverViewItem.reset_label (); 453 GlyphCanvas.redraw (); 454 } 455 456 public override void zoom_in () { 457 OverViewItem.width *= 1.1; 458 OverViewItem.height *= 1.1; 459 OverViewItem.margin *= 1.1; 460 update_item_list (); 461 OverViewItem.reset_label (); 462 GlyphCanvas.redraw (); 463 update_zoom_bar (); 464 } 465 466 public override void zoom_out () { 467 OverViewItem.width *= 0.9; 468 OverViewItem.height *= 0.9; 469 OverViewItem.margin *= 0.9; 470 update_item_list (); 471 OverViewItem.reset_label (); 472 GlyphCanvas.redraw (); 473 update_zoom_bar (); 474 } 475 476 public override void store_current_view () { 477 } 478 479 public override void restore_last_view () { 480 } 481 482 public override void next_view () { 483 } 484 485 public override string get_label () { 486 return t_("Overview"); 487 } 488 489 public override string get_name () { 490 return "Overview"; 491 } 492 493 public void display_all_available_glyphs () { 494 all_available = true; 495 496 view_offset_y = 0; 497 first_visible = 0; 498 selected = 0; 499 500 update_item_list (); 501 selected_item = get_selected_item (); 502 GlyphCanvas.redraw (); 503 } 504 505 OverViewItem get_selected_item () { 506 if (visible_items.size == 0) { 507 return new OverViewItem (); 508 } 509 510 if (!(0 <= selected < visible_items.size)) { 511 return selected_item; 512 } 513 514 OverViewItem item = visible_items.get (selected); 515 item.selected = true; 516 return item; 517 } 518 519 int get_items_per_row () { 520 int i = 1; 521 double tab_with = allocation.width - 30; // 30 px for the scroll bar 522 OverViewItem.margin = OverViewItem.width * 0.1; 523 double l = OverViewItem.margin + OverViewItem.full_width (); 524 525 while (l <= tab_with) { 526 l += OverViewItem.full_width (); 527 i++; 528 } 529 530 return i - 1; 531 } 532 533 public void update_item_list () { 534 update_scheduled = true; 535 } 536 537 public void process_item_list_update () { 538 string character_string; 539 Font f = BirdFont.get_current_font (); 540 GlyphCollection? glyphs = null; 541 uint32 index; 542 OverViewItem item; 543 double x, y; 544 unichar character; 545 Glyph glyph; 546 double tab_with; 547 int item_list_length; 548 int visible_size; 549 550 tab_with = allocation.width - 30; // scrollbar 551 552 items_per_row = get_items_per_row (); 553 rows = (int) (allocation.height / OverViewItem.full_height ()) + 2; 554 555 item_list_length = items_per_row * rows; 556 visible_items.clear (); 557 558 index = (uint32) first_visible; 559 x = OverViewItem.margin; 560 y = OverViewItem.margin; 561 562 if (all_available) { 563 uint font_length = f.length (); 564 565 for (int i = 0; i < item_list_length && index < font_length; i++) { 566 glyphs = f.get_glyph_collection_index ((uint32) index); 567 return_if_fail (glyphs != null); 568 569 glyph = ((!) glyphs).get_current (); 570 character_string = glyph.name; 571 character = glyph.unichar_code; 572 573 item = new OverViewItem (); 574 item.set_character (character); 575 item.set_glyphs (glyphs); 576 item.x = x; 577 item.y = y; 578 visible_items.add (item); 579 index++; 580 } 581 } else { 582 uint32 glyph_range_size = glyph_range.get_length (); 583 584 uint max_length = glyph_range.length () - first_visible; 585 586 if (item_list_length > max_length) { 587 item_list_length = (int) max_length; 588 } 589 590 for (int i = 0; i < item_list_length && index < glyph_range_size; i++) { 591 item = new OverViewItem (); 592 visible_items.add (item); 593 } 594 595 index = (uint32) first_visible; 596 visible_size = visible_items.size; 597 for (int i = 0; i < visible_size; i++) { 598 item = visible_items.get (i); 599 character = glyph_range.get_character ((uint32) index); 600 item.set_character (character); 601 index++; 602 } 603 604 visible_size = visible_items.size; 605 for (int i = 0; i < visible_size; i++) { 606 item = visible_items.get (i); 607 glyphs = f.get_glyph_collection_by_name ((!) item.character.to_string ()); 608 item.set_glyphs (glyphs); 609 } 610 } 611 612 x = OverViewItem.margin; 613 y = OverViewItem.margin; 614 615 visible_size = visible_items.size; 616 int selected_index; 617 bool selected_item; 618 double full_width = OverViewItem.full_width (); 619 620 for (int i = 0; i < visible_size; i++) { 621 item = visible_items.get (i); 622 623 selected_item = false; 624 625 if (all_available) { 626 glyphs = f.get_glyph_collection_index ((uint32) i); 627 } else { 628 glyphs = f.get_glyph_collection_by_name ((!) item.character.to_string ()); 629 } 630 631 if (glyphs != null) { 632 selected_index = selected_items.index_of ((!) glyphs); 633 selected_item = (selected_index != -1); 634 } 635 636 item.adjust_scale (); 637 638 selected_item |= (i == selected); 639 item.selected = selected_item; 640 641 item.x = x + view_offset_x; 642 item.y = y + view_offset_y; 643 644 x += full_width; 645 646 if (x + full_width >= tab_with) { 647 x = OverViewItem.margin; 648 y += OverViewItem.full_height (); 649 } 650 } 651 652 update_scheduled = false; 653 } 654 655 public override void draw (WidgetAllocation allocation, Context cr) { 656 if (update_scheduled 657 || this.allocation.width != allocation.width 658 || this.allocation.height != allocation.height 659 || this.allocation.width == 0) { 660 this.allocation = allocation; 661 process_item_list_update (); 662 } 663 664 this.allocation = allocation; 665 666 // clear canvas 667 cr.save (); 668 Theme.color (cr, "Background 1"); 669 cr.rectangle (0, 0, allocation.width, allocation.height); 670 cr.fill (); 671 cr.restore (); 672 673 foreach (OverViewItem i in visible_items) { 674 i.draw (allocation, cr); 675 } 676 677 if (unlikely (visible_items.size == 0)) { 678 draw_empty_canvas (allocation, cr); 679 } 680 681 if (unlikely (character_info != null)) { 682 draw_character_info (cr); 683 } 684 } 685 686 void draw_empty_canvas (WidgetAllocation allocation, Context cr) { 687 Text t; 688 689 cr.save (); 690 t = new Text (t_("No glyphs in this view."), 24); 691 Theme.text_color (t, "Text Foreground"); 692 t.widget_x = 40; 693 t.widget_y = 30; 694 t.draw (cr); 695 cr.restore (); 696 } 697 698 public void scroll_rows (int row_adjustment) { 699 for (int i = 0; i < row_adjustment; i++) { 700 scroll (-OverViewItem.height); 701 } 702 703 for (int i = 0; i > row_adjustment; i--) { 704 scroll (OverViewItem.height); 705 } 706 } 707 708 public void scroll_adjustment (double pixel_adjustment) { 709 double l; 710 Font f; 711 712 if (all_available) { 713 f = BirdFont.get_current_font (); 714 l = f.length (); 715 } else { 716 l = glyph_range.length (); 717 } 718 719 if (first_visible <= 0) { 720 return; 721 } 722 723 if (first_visible + rows * items_per_row >= l) { 724 return; 725 } 726 727 scroll ((int64) pixel_adjustment); 728 } 729 730 void scroll_to_position (int64 r) { 731 if (r < 0) { 732 scroll_top (); 733 return; 734 } 735 736 selected -= (int) (r - first_visible); 737 first_visible = (int) r; 738 update_item_list (); 739 } 740 741 public override void scroll_to (double position) requires (items_per_row > 0) { 742 double r; 743 int nrows; 744 Font f; 745 746 if (all_available) { 747 f = BirdFont.get_current_font (); 748 nrows = (int) (f.length () / items_per_row); 749 } else { 750 nrows = (int) (glyph_range.length () / items_per_row); 751 } 752 753 view_offset_y = 0; 754 r = (int64) (position * (nrows - rows + 3)); // 3 invisible rows 755 r *= items_per_row; 756 757 scroll_to_position ((int64) r); 758 update_item_list (); 759 GlyphCanvas.redraw (); 760 } 761 762 private void scroll (double pixel_adjustment) { 763 if (first_visible < 0 && pixel_adjustment < 0) { 764 scroll_top (); 765 return; 766 } 767 768 view_offset_y += pixel_adjustment; 769 770 if (view_offset_y >= 0) { 771 while (view_offset_y > OverViewItem.height) { 772 view_offset_y -= OverViewItem.height; 773 first_visible -= items_per_row; 774 } 775 776 first_visible -= items_per_row; 777 view_offset_y -= OverViewItem.height; 778 } else if (view_offset_y < -OverViewItem.height) { 779 view_offset_y = 0; 780 first_visible += items_per_row; 781 } 782 783 update_item_list (); 784 } 785 786 public void scroll_top () { 787 first_visible = 0; 788 view_offset_y = 0; 789 790 update_item_list (); 791 792 if (visible_items.size != 0) { 793 selected_item = get_selected_item (); 794 } 795 } 796 797 /** Returns true if the selected glyph is at the last row. */ 798 private bool last_row () { 799 return visible_items.size - selected <= items_per_row; 800 } 801 802 public void key_down () { 803 Font f = BirdFont.get_current_font (); 804 int64 len = (all_available) ? f.length () : glyph_range.length (); 805 806 if (at_bottom () && last_row ()) { 807 return; 808 } 809 810 selected += items_per_row; 811 812 if (selected >= items_per_row * rows) { 813 first_visible += items_per_row; 814 selected -= items_per_row; 815 } 816 817 if (first_visible + selected >= len) { 818 selected = (int) (len - first_visible - 1); 819 820 if (selected < items_per_row * (rows - 1)) { 821 first_visible -= items_per_row; 822 selected += items_per_row; 823 } 824 } 825 826 if (selected >= visible_items.size) { 827 selected = (int) (visible_items.size - 1); 828 } 829 830 selected_item = get_selected_item (); 831 update_item_list (); 832 } 833 834 public void key_right () { 835 Font f = BirdFont.get_current_font (); 836 int64 len = (all_available) ? f.length () : glyph_range.length (); 837 838 if (at_bottom () && first_visible + selected + 1 >= len) { 839 selected = (int) (visible_items.size - 1); 840 selected_item = get_selected_item (); 841 return; 842 } 843 844 selected += 1; 845 846 if (selected >= items_per_row * rows) { 847 first_visible += items_per_row; 848 selected -= items_per_row; 849 selected -= 1; 850 } 851 852 if (first_visible + selected > len) { 853 first_visible -= items_per_row; 854 selected = (int) (len - first_visible - 1); 855 selected_item = get_selected_item (); 856 } 857 update_item_list (); 858 } 859 860 public void key_up () { 861 selected -= items_per_row; 862 863 if (selected < 0) { 864 first_visible -= items_per_row; 865 selected += items_per_row; 866 } 867 868 if (first_visible < 0) { 869 first_visible = 0; 870 } 871 update_item_list (); 872 } 873 874 public void key_left () { 875 selected -= 1; 876 877 if (selected < 0) { 878 first_visible -= items_per_row; 879 selected += items_per_row; 880 selected += 1; 881 } 882 883 if (first_visible < 0) { 884 scroll_top (); 885 } 886 update_item_list (); 887 } 888 889 public string get_selected_char () { 890 Font f; 891 Glyph? g; 892 893 if (all_available) { 894 f = BirdFont.get_current_font (); 895 g = f.get_glyph_index (selected); 896 return_val_if_fail (g != null, "".dup ()); 897 return ((!) g).get_name (); 898 } 899 900 return glyph_range.get_char (selected); 901 } 902 903 public override void key_press (uint keyval) { 904 hide_menu (); 905 update_item_list (); 906 GlyphCanvas.redraw (); 907 908 if (KeyBindings.has_ctrl () || KeyBindings.has_logo ()) { 909 return; 910 } 911 912 switch (keyval) { 913 case Key.ENTER: 914 open_current_glyph (); 915 return; 916 917 case Key.UP: 918 get_selected_item ().selected = false; 919 920 key_up (); 921 selected_item = get_selected_item (); 922 923 selected_items.clear (); 924 if (selected_item.glyphs != null) { 925 selected_items.add ((!) selected_item.glyphs); 926 } 927 928 update_scrollbar (); 929 return; 930 931 case Key.RIGHT: 932 get_selected_item ().selected = false; 933 934 key_right (); 935 selected_item = get_selected_item (); 936 937 selected_items.clear (); 938 if (selected_item.glyphs != null) { 939 selected_items.add ((!) selected_item.glyphs); 940 } 941 942 update_scrollbar (); 943 return; 944 945 case Key.LEFT: 946 get_selected_item ().selected = false; 947 948 key_left (); 949 selected_item = get_selected_item (); 950 951 selected_items.clear (); 952 if (selected_item.glyphs != null) { 953 selected_items.add ((!) selected_item.glyphs); 954 } 955 956 update_scrollbar(); 957 return; 958 959 case Key.DOWN: 960 get_selected_item ().selected = false; 961 962 key_down (); 963 selected_item = get_selected_item (); 964 965 selected_items.clear (); 966 if (selected_item.glyphs != null) { 967 selected_items.add ((!) selected_item.glyphs); 968 } 969 970 update_scrollbar (); 971 return; 972 973 case Key.PG_UP: 974 get_selected_item ().selected = false; 975 976 for (int i = 0; i < rows; i++) { 977 key_up (); 978 } 979 selected_item = get_selected_item (); 980 981 selected_items.clear (); 982 if (selected_item.glyphs != null) { 983 selected_items.add ((!) selected_item.glyphs); 984 } 985 986 update_scrollbar (); 987 return; 988 989 case Key.PG_DOWN: 990 get_selected_item ().selected = false; 991 992 for (int i = 0; i < rows; i++) { 993 key_down (); 994 } 995 selected_item = get_selected_item (); 996 997 selected_items.clear (); 998 if (selected_item.glyphs != null) { 999 selected_items.add ((!) selected_item.glyphs); 1000 } 1001 1002 update_scrollbar (); 1003 return; 1004 1005 case Key.DEL: 1006 delete_selected_glyph (); 1007 selected_item = get_selected_item (); 1008 return; 1009 1010 case Key.BACK_SPACE: 1011 delete_selected_glyph (); 1012 selected_item = get_selected_item (); 1013 return; 1014 } 1015 1016 if (!KeyBindings.has_ctrl () && !KeyBindings.has_logo ()) { 1017 scroll_to_char (keyval); 1018 } 1019 1020 selected_item = get_selected_item (); 1021 1022 selected_items.clear (); 1023 if (selected_item.glyphs != null) { 1024 selected_items.add ((!) selected_item.glyphs); 1025 } 1026 1027 update_item_list (); 1028 GlyphCanvas.redraw (); 1029 } 1030 1031 public void delete_selected_glyph () { 1032 Font font = BirdFont.get_current_font (); 1033 OverViewUndoItem undo_item = new OverViewUndoItem (); 1034 1035 undo_item.alternate_sets = font.alternates.copy (); 1036 1037 foreach (GlyphCollection g in selected_items) { 1038 undo_item.glyphs.add (g.copy ()); 1039 } 1040 store_undo_items (undo_item); 1041 1042 foreach (GlyphCollection glyph_collection in selected_items) { 1043 font.delete_glyph (glyph_collection); 1044 string name = glyph_collection.get_name (); 1045 MainWindow.get_tab_bar ().close_background_tab_by_name (name); 1046 } 1047 1048 update_item_list (); 1049 GlyphCanvas.redraw (); 1050 } 1051 1052 public override void undo () { 1053 Font font = BirdFont.get_current_font (); 1054 OverViewUndoItem previous_collection; 1055 1056 if (undo_items.size == 0) { 1057 return; 1058 } 1059 1060 previous_collection = undo_items.get (undo_items.size - 1); 1061 redo_items.add (get_current_state (previous_collection)); 1062 1063 // remove the old glyph and add the new one 1064 foreach (GlyphCollection g in previous_collection.glyphs) { 1065 font.delete_glyph (g); 1066 1067 if (g.length () > 0) { 1068 font.add_glyph_collection (g); 1069 } 1070 1071 TabBar tabs = MainWindow.get_tab_bar (); 1072 Tab? tab = tabs.get_tab (g.get_name ()); 1073 1074 if (tab != null) { 1075 Tab t = (!) tab; 1076 set_glyph_zoom (g); 1077 t.set_glyph_collection (g); 1078 t.set_display (new GlyphTab (g)); 1079 } 1080 } 1081 1082 Font f = BirdFont.get_current_font (); 1083 f.alternates = previous_collection.alternate_sets.copy (); 1084 1085 undo_items.remove_at (undo_items.size - 1); 1086 GlyphCanvas.redraw (); 1087 } 1088 1089 public override void redo () { 1090 Font font = BirdFont.get_current_font (); 1091 OverViewUndoItem previous_collection; 1092 1093 if (redo_items.size == 0) { 1094 return; 1095 } 1096 1097 previous_collection = redo_items.get (redo_items.size - 1); 1098 undo_items.add (get_current_state (previous_collection)); 1099 1100 // remove the old glyph and add the new one 1101 foreach (GlyphCollection g in previous_collection.glyphs) { 1102 font.delete_glyph (g); 1103 font.add_glyph_collection (g); 1104 1105 TabBar tabs = MainWindow.get_tab_bar (); 1106 Tab? tab = tabs.get_tab (g.get_name ()); 1107 1108 if (tab != null) { 1109 Tab t = (!) tab; 1110 set_glyph_zoom (g); 1111 t.set_glyph_collection (g); 1112 t.set_display (new GlyphTab (g)); 1113 } 1114 } 1115 font.alternates = previous_collection.alternate_sets.copy (); 1116 1117 redo_items.remove_at (redo_items.size - 1); 1118 GlyphCanvas.redraw (); 1119 } 1120 1121 public OverViewUndoItem get_current_state (OverViewUndoItem previous_collection) { 1122 GlyphCollection? gc; 1123 OverViewUndoItem ui = new OverViewUndoItem (); 1124 Font font = BirdFont.get_current_font (); 1125 1126 ui.alternate_sets = font.alternates.copy (); 1127 1128 foreach (GlyphCollection g in previous_collection.glyphs) { 1129 gc = font.get_glyph_collection (g.get_name ()); 1130 1131 if (gc != null) { 1132 ui.glyphs.add (((!) gc).copy ()); 1133 } else { 1134 ui.glyphs.add (new GlyphCollection (g.get_unicode_character (), g.get_name ())); 1135 } 1136 } 1137 1138 return ui; 1139 } 1140 1141 public void store_undo_state (GlyphCollection gc) { 1142 OverViewUndoItem i = new OverViewUndoItem (); 1143 Font f = BirdFont.get_current_font (); 1144 i.alternate_sets = f.alternates.copy (); 1145 i.glyphs.add (gc); 1146 store_undo_items (i); 1147 } 1148 1149 public void store_undo_items (OverViewUndoItem i) { 1150 undo_items.add (i); 1151 redo_items.clear (); 1152 } 1153 1154 bool select_visible_glyph (string name) { 1155 int i = 0; 1156 1157 foreach (OverViewItem o in visible_items) { 1158 if (o.get_name () == name) { 1159 selected = i; 1160 selected_item = get_selected_item (); 1161 1162 if (selected_item.y > allocation.height - OverViewItem.height) { 1163 view_offset_y -= (selected_item.y + OverViewItem.height) - allocation.height; 1164 } 1165 1166 if (selected_item.y < 0) { 1167 view_offset_y = 0; 1168 } 1169 1170 return true; 1171 } 1172 1173 if (i > 1000) { 1174 warning ("selected character not found"); 1175 return true; 1176 } 1177 1178 i++; 1179 } 1180 1181 return false; 1182 } 1183 1184 public void scroll_to_char (unichar c) { 1185 StringBuilder s = new StringBuilder (); 1186 1187 if (is_modifier_key (c)) { 1188 return; 1189 } 1190 1191 s.append_unichar (c); 1192 scroll_to_glyph (s.str); 1193 } 1194 1195 public void scroll_to_glyph (string name) { 1196 GlyphRange gr = glyph_range; 1197 int i, r, index; 1198 string ch; 1199 Font font = BirdFont.get_current_font (); 1200 GlyphCollection? glyphs = null; 1201 Glyph glyph; 1202 1203 index = -1; 1204 1205 if (items_per_row <= 0) { 1206 return; 1207 } 1208 1209 ch = name; 1210 1211 // selected char is visible 1212 if (select_visible_glyph (ch)) { 1213 return; 1214 } 1215 1216 // scroll to char 1217 if (all_available) { 1218 1219 // don't search for glyphs in huge CJK fonts 1220 if (font.length () > 500) { 1221 r = 0; 1222 } else { 1223 // FIXME: too slow 1224 for (r = 0; r < font.length (); r += items_per_row) { 1225 for (i = 0; i < items_per_row && i < font.length (); i++) { 1226 glyphs = font.get_glyph_collection_index ((uint32) r + i); 1227 return_if_fail (glyphs != null); 1228 glyph = ((!) glyphs).get_current (); 1229 1230 if (glyph.name == ch) { 1231 index = i; 1232 } 1233 } 1234 1235 if (index > -1) { 1236 break; 1237 } 1238 } 1239 } 1240 } else { 1241 1242 if (ch.char_count () > 1) { 1243 warning ("Can't scroll to ligature in this view"); 1244 return; 1245 } 1246 1247 for (r = 0; r < gr.length (); r += items_per_row) { 1248 for (i = 0; i < items_per_row; i++) { 1249 if (gr.get_char (r + i) == ch) { 1250 index = i; 1251 } 1252 } 1253 1254 if (index > -1) { 1255 break; 1256 } 1257 } 1258 } 1259 1260 if (index > -1) { 1261 first_visible = r; 1262 process_item_list_update (); 1263 update_item_list (); 1264 select_visible_glyph (ch); 1265 } 1266 } 1267 1268 public override void double_click (uint button, double ex, double ey) 1269 requires (!is_null (visible_items) && !is_null (allocation)) { 1270 1271 return_if_fail (!is_null (this)); 1272 1273 foreach (OverViewItem i in visible_items) { 1274 if (i.double_click (button, ex, ey)) { 1275 open_overview_item (i); 1276 } 1277 } 1278 1279 GlyphCanvas.redraw (); 1280 } 1281 1282 public void open_overview_item (OverViewItem i) { 1283 return_if_fail (!is_null (i)); 1284 1285 if (i.glyphs != null) { 1286 open_glyph_signal ((!) i.glyphs); 1287 GlyphCollection gc = (!) i.glyphs; 1288 gc.get_current ().close_path (); 1289 } else { 1290 open_new_glyph_signal (i.character); 1291 } 1292 } 1293 1294 public void set_character_info (CharacterInfo i) { 1295 character_info = i; 1296 } 1297 1298 public int get_selected_index () { 1299 GlyphCollection gc; 1300 int index = 0; 1301 1302 if (selected_items.size == 0) { 1303 return 0; 1304 } 1305 1306 gc = selected_items.get (0); 1307 1308 foreach (OverViewItem i in visible_items) { 1309 if (i.glyphs != null && gc == ((!) i.glyphs)) { 1310 break; 1311 } 1312 1313 index++; 1314 } 1315 1316 return index; 1317 } 1318 1319 public void hide_menu () { 1320 foreach (OverViewItem i in visible_items) { 1321 i.hide_menu (); 1322 } 1323 } 1324 1325 public override void button_press (uint button, double x, double y) { 1326 OverViewItem i; 1327 int index = 0; 1328 int selected_index = -1; 1329 bool update = false; 1330 1331 if (character_info != null) { 1332 character_info = null; 1333 GlyphCanvas.redraw (); 1334 return; 1335 } 1336 1337 if (!KeyBindings.has_shift ()) { 1338 selected_items.clear (); 1339 } 1340 1341 for (int j = 0; j < visible_items.size; j++) { 1342 i = visible_items.get (j); 1343 1344 if (i.click (button, x, y)) { 1345 selected = index; 1346 selected_item = get_selected_item (); 1347 1348 if (KeyBindings.has_shift ()) { 1349 if (selected_item.glyphs != null) { 1350 1351 selected_index = selected_items.index_of ((!) selected_item.glyphs); 1352 if (selected_index == -1) { 1353 selected_items.add ((!) selected_item.glyphs); 1354 } else { 1355 return_if_fail (0 <= selected_index < selected_items.size); 1356 selected_items.remove_at (selected_index); 1357 selected = get_selected_index (); 1358 selected_item = get_selected_item (); 1359 } 1360 } 1361 } else { 1362 selected_items.clear (); 1363 if (selected_item.glyphs != null) { 1364 selected_items.add ((!) selected_item.glyphs); 1365 } 1366 } 1367 1368 if (!is_null (i.version_menu)) { 1369 update = !((!)i).version_menu.menu_visible; 1370 } else { 1371 update = true; 1372 } 1373 } 1374 index++; 1375 } 1376 1377 if (update) { 1378 update_item_list (); 1379 } 1380 1381 GlyphCanvas.redraw (); 1382 } 1383 1384 /** Returns true if overview shows the last character. */ 1385 private bool at_bottom () { 1386 Font f; 1387 double t = rows * items_per_row + first_visible; 1388 1389 if (all_available) { 1390 f = BirdFont.get_current_font (); 1391 return t >= f.length (); 1392 } 1393 1394 return t >= glyph_range.length (); 1395 } 1396 1397 public void set_current_glyph_range (GlyphRange range) { 1398 GlyphRange? current = glyph_range; 1399 string c; 1400 1401 if (current != null) { 1402 c = glyph_range.get_char (selected); 1403 } 1404 1405 all_available = false; 1406 1407 glyph_range = range; 1408 scroll_top (); 1409 1410 // TODO: scroll down to c 1411 update_item_list (); 1412 selected_item = get_selected_item (); 1413 1414 GlyphCanvas.redraw (); 1415 } 1416 1417 public void select_next_glyph () { 1418 key_right (); 1419 } 1420 1421 public void open_current_glyph () { 1422 // keep this object even if open_glyph_signal closes the display 1423 this.ref (); 1424 1425 selected_item = get_selected_item (); 1426 if (selected_item.glyphs != null) { 1427 open_glyph_signal ((!) selected_item.glyphs); 1428 GlyphCollection? gc2 = selected_item.glyphs; 1429 GlyphCollection gc = (!) selected_item.glyphs; 1430 gc.get_current ().close_path (); 1431 } else { 1432 open_new_glyph_signal (selected_item.character); 1433 } 1434 1435 this.unref (); 1436 } 1437 1438 public override void update_scrollbar () { 1439 Font f; 1440 double nrows = 0; 1441 double pos = 0; 1442 double size; 1443 double visible_rows; 1444 1445 if (rows == 0) { 1446 MainWindow.set_scrollbar_size (0); 1447 MainWindow.set_scrollbar_position (0); 1448 } else { 1449 if (all_available) { 1450 f = BirdFont.get_current_font (); 1451 nrows = Math.floor ((f.length ()) / rows); 1452 size = f.length (); 1453 } else { 1454 nrows = Math.floor ((glyph_range.length ()) / rows); 1455 size = glyph_range.length (); 1456 } 1457 1458 if (nrows <= 0) { 1459 nrows = 1; 1460 } 1461 1462 visible_rows = allocation.height / OverViewItem.height; 1463 scroll_size = visible_rows / nrows; 1464 MainWindow.set_scrollbar_size (scroll_size); 1465 pos = first_visible / (nrows * items_per_row - visible_rows * items_per_row); 1466 MainWindow.set_scrollbar_position (pos); 1467 } 1468 } 1469 1470 /** Display one entry from the Unicode Character Database. */ 1471 void draw_character_info (Context cr) 1472 requires (character_info != null) { 1473 double x, y, w, h; 1474 int i; 1475 string unicode_value, unicode_description; 1476 string[] column; 1477 string entry; 1478 int len = 0; 1479 int length = 0; 1480 bool see_also = false; 1481 WidgetAllocation allocation = MainWindow.get_overview ().allocation; 1482 string name; 1483 string[] lines; 1484 double character_start; 1485 double character_height; 1486 1487 entry = ((!)character_info).get_entry (); 1488 lines = entry.split ("\n"); 1489 1490 foreach (string line in entry.split ("\n")) { 1491 len = line.char_count (); 1492 if (len > length) { 1493 length = len; 1494 } 1495 } 1496 1497 x = allocation.width * 0.1; 1498 y = allocation.height * 0.1; 1499 w = allocation.width * 0.9 - x; 1500 h = allocation.height * 0.9 - y; 1501 1502 if (w < 8 * length) { 1503 w = 8 * length; 1504 x = (allocation.width - w) / 2.0; 1505 } 1506 1507 if (x < 0) { 1508 x = 2; 1509 } 1510 1511 // background 1512 cr.save (); 1513 Theme.color_opacity (cr, "Background 1", 0.98); 1514 cr.rectangle (x, y, w, h); 1515 cr.fill (); 1516 cr.restore (); 1517 1518 cr.save (); 1519 Theme.color_opacity (cr, "Foreground 1", 0.98); 1520 cr.set_line_width (2); 1521 cr.rectangle (x, y, w, h); 1522 cr.stroke (); 1523 cr.restore (); 1524 1525 // database entry 1526 1527 if (((!)character_info).is_ligature ()) { 1528 name = ((!)character_info).get_name (); 1529 draw_info_line (name, cr, x, y, 0); 1530 } else { 1531 i = 0; 1532 foreach (string line in lines) { 1533 if (i == 0) { 1534 column = line.split ("\t"); 1535 return_if_fail (column.length == 2); 1536 unicode_value = "U+" + column[0]; 1537 unicode_description = column[1]; 1538 1539 draw_info_line (unicode_description, cr, x, y, i); 1540 i++; 1541 1542 draw_info_line (unicode_value, cr, x, y, i); 1543 i++; 1544 } else { 1545 1546 if (line.has_prefix ("\t*")) { 1547 draw_info_line (line.replace ("\t*", "•"), cr, x, y, i); 1548 i++; 1549 } else if (line.has_prefix ("\tx (")) { 1550 if (!see_also) { 1551 i++; 1552 draw_info_line (t_("See also:"), cr, x, y, i); 1553 i++; 1554 see_also = true; 1555 } 1556 1557 draw_info_line (line.replace ("\tx (", "•").replace (")", ""), cr, x, y, i); 1558 i++; 1559 } else { 1560 i++; 1561 } 1562 } 1563 } 1564 1565 character_start = y + 10 + i * UCD_LINE_HEIGHT; 1566 character_height = h - character_start; 1567 draw_fallback_character (cr, x, character_start, character_height); 1568 } 1569 } 1570 1571 /** Fallback character in UCD info. */ 1572 void draw_fallback_character (Context cr, double x, double y, double height) 1573 requires (character_info != null) { 1574 unichar c = ((!)character_info).unicode; 1575 1576 cr.save (); 1577 Text character = new Text (); 1578 character.set_use_cache (false); 1579 Theme.text_color (character, "Foreground 1"); 1580 character.set_text ((!) c.to_string ()); 1581 character.set_font_size (height); 1582 character.draw_at_top (cr, x + 10, y); 1583 cr.restore (); 1584 } 1585 1586 void draw_info_line (string line, Context cr, double x, double y, int row) { 1587 Text ucd_entry = new Text (line); 1588 cr.save (); 1589 Theme.text_color (ucd_entry, "Foreground 1"); 1590 ucd_entry.widget_x = 10 + x; 1591 ucd_entry.widget_y = 10 + y + row * UCD_LINE_HEIGHT; 1592 ucd_entry.draw (cr); 1593 cr.restore (); 1594 } 1595 1596 public void paste () { 1597 GlyphCollection gc; 1598 GlyphCollection? c; 1599 Glyph glyph; 1600 uint32 index; 1601 int i; 1602 int skip = 0; 1603 int s; 1604 string character_string; 1605 Gee.ArrayList<GlyphCollection> glyps; 1606 Font f; 1607 OverViewUndoItem undo_item; 1608 1609 f = BirdFont.get_current_font (); 1610 gc = new GlyphCollection ('\0', ""); 1611 glyps = new Gee.ArrayList<GlyphCollection> (); 1612 1613 copied_glyphs.sort ((a, b) => { 1614 return (int) ((GlyphCollection) a).get_unicode_character () 1615 - (int) ((GlyphCollection) b).get_unicode_character (); 1616 }); 1617 1618 index = (uint32) first_visible + selected; 1619 for (i = 0; i < copied_glyphs.size; i++) { 1620 if (all_available) { 1621 if (f.length () == 0) { 1622 c = add_empty_character_to_font (copied_glyphs.get (i).get_unicode_character (), 1623 copied_glyphs.get (i).is_unassigned (), 1624 copied_glyphs.get (i).get_name ()); 1625 } else if (index >= f.length ()) { 1626 // FIXME: duplicated unicodes? 1627 c = add_empty_character_to_font (copied_glyphs.get (i).get_unicode_character (), 1628 copied_glyphs.get (i).is_unassigned (), 1629 copied_glyphs.get (i).get_name ()); 1630 } else { 1631 c = f.get_glyph_collection_index ((uint32) index); 1632 } 1633 1634 if (c == null) { 1635 c = add_empty_character_to_font (copied_glyphs.get (i).get_unicode_character (), 1636 copied_glyphs.get (i).is_unassigned (), 1637 copied_glyphs.get (i).get_name ()); 1638 } 1639 1640 return_if_fail (c != null); 1641 gc = (!) c; 1642 } else { 1643 if (i != 0) { 1644 s = (int) copied_glyphs.get (i).get_unicode_character (); 1645 s -= (int) copied_glyphs.get (i - 1).get_unicode_character (); 1646 s -= 1; 1647 skip += s; 1648 } 1649 1650 character_string = glyph_range.get_char ((uint32) (index + skip)); 1651 c = f.get_glyph_collection_by_name (character_string); 1652 1653 if (c == null) { 1654 gc = add_empty_character_to_font (character_string.get_char (), 1655 copied_glyphs.get (i).is_unassigned (), 1656 copied_glyphs.get (i).get_name ()); 1657 } else { 1658 gc = (!) c; 1659 } 1660 } 1661 1662 glyps.add (gc); 1663 index++; 1664 } 1665 1666 undo_item = new OverViewUndoItem (); 1667 undo_item.alternate_sets = f.alternates.copy (); 1668 foreach (GlyphCollection g in glyps) { 1669 undo_item.glyphs.add (g.copy ()); 1670 } 1671 store_undo_items (undo_item); 1672 1673 if (glyps.size != copied_glyphs.size) { 1674 warning ("glyps.size != copied_glyphs.size"); 1675 return; 1676 } 1677 1678 if (copied_glyphs.size < i) { 1679 warning ("Array index out of bounds."); 1680 return; 1681 } 1682 1683 i = 0; 1684 foreach (GlyphCollection g in glyps) { 1685 glyph = copied_glyphs.get (i).get_current ().copy (); 1686 glyph.version_id = (glyph.version_id == -1 || g.length () == 0) ? 1 : g.get_last_id () + 1; 1687 glyph.unichar_code = g.get_unicode_character (); 1688 1689 if (!g.is_unassigned ()) { 1690 glyph.name = (!) glyph.unichar_code.to_string (); 1691 } else { 1692 glyph.name = g.get_name (); 1693 } 1694 1695 g.insert_glyph (glyph, true); 1696 i++; 1697 } 1698 1699 f.touch (); 1700 1701 update_item_list (); 1702 GlyphCanvas.redraw (); 1703 } 1704 1705 public class OverViewUndoItem { 1706 public AlternateSets alternate_sets = new AlternateSets (); 1707 public Gee.ArrayList<GlyphCollection> glyphs = new Gee.ArrayList<GlyphCollection> (); 1708 } 1709 } 1710 1711 } 1712