From 691ab989638ff10484d96b3308b509fecd9ec1c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jul 2008 10:47:19 +0000 Subject: [PATCH] better UI for TeX/Unicode and terms grammar --- helm/software/matita/dist/ChangeLog | 1 + helm/software/matita/matita.glade | 7031 ++++++++++++++---------- helm/software/matita/matitaGtkMisc.ml | 26 + helm/software/matita/matitaGtkMisc.mli | 2 +- helm/software/matita/matitaGui.ml | 33 +- 5 files changed, 4102 insertions(+), 2991 deletions(-) diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 5c563376c..580d410fc 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -6,6 +6,7 @@ * notation for lists fixed to add a break point after the separator * notation for the existential is now user definable * \infrule layout added, allows to display readable fractions + * better window for terms grammar and TeX/Unicode 0.5.2 - 2/7/2008 - better-usability-for-the-working-constructivist release * refinement of match fixed to prevent useless unfolding, diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 8cd2a9a73..373ebb433 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1,2969 +1,4066 @@ - - - + + + - - True - Cic browser - GTK_WIN_POS_CENTER_ON_PARENT - 500 - 500 - - - True - - - True - - - True - - - True - _File - True - - - - - True - gtk-new - True - True - - - - - True - Open _Location ... - True - - - - - - True - - - - - True - gtk-close - True - True - - - - - - - - - True - _Edit - True - - - - - True - gtk-copy - True - True - - - - - - - - - True - _View - True - - - - - True - _Metadata - True - - - - - True - View the graph of objects on which the current one depends on - (Direct) Dependencies - True - - - - - True - View the graph of objects which depends on the current one - (Inverse) Dependencies - True - - - - - True - - - - - True - HBugs Tutors - True - - - - - - - - - False - False - - - - - True - 0 - 0 - GTK_SHADOW_NONE - - - True - - - True - True - GTK_RELIEF_NONE - 0 - - - True - gtk-new - - - - - False - False - - - - - True - True - GTK_RELIEF_NONE - 0 - - - True - gtk-go-back - - - - - False - False - 1 - - - - - True - True - GTK_RELIEF_NONE - 0 - - - True - gtk-go-forward - - - - - False - False - 2 - - - - - True - True - True - refresh - GTK_RELIEF_NONE - 0 - - - True - gtk-refresh - - - - - False - False - 3 - - - - - True - True - True - home - GTK_RELIEF_NONE - 0 - - - True - gtk-home - - - - - False - False - 4 - - - - - True - gtk-jump-to - 2 - - - False - False - 3 - 5 - - - - - True - - - - - - 6 - - - - - - - False - 1 - - - - - True - 3 - 6 - - - True - gtk-missing-image - - - False - - - - - True - True - * - - - 1 - - - - - True - - - True - - - - - - False - False - - - - - False - 2 - - - - - False - 2 - - - - - True - True - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - - - - False - - - - - True - MathView - - - tab - False - False - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - - - True - True - False - - - - - 1 - False - - - - - True - WhelpResults - - - tab - 1 - False - False - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - True - GTK_SHADOW_NONE - - - True - gtk-missing-image - - - - - - - 2 - False - - - - - True - WhelpEasterEgg - - - tab - 2 - False - False - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - - - - 3 - False - - - - - True - Graph - - - tab - 3 - False - False - - - - - True - - - True - True - - - True - True - - - - - - - True - GTK_TOOLBAR_BOTH - - - True - - - True - True - gtk-refresh - True - 0 - - - - - False - False - - - - - True - - - True - True - gtk-remove - True - 0 - - - - - False - False - - - - - True - - - True - True - gtk-add - True - 0 - - - - - False - False - - - - - False - False - 1 - - - - - 4 - False - - - - - True - HBugs - - - tab - 4 - False - False - - - - - 3 - - - - - - - - - DUMMY - False - True - GTK_WIN_POS_CENTER - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - - - True - DUMMY - GTK_JUSTIFY_CENTER - - - False - False - 2 - - - - - True - GTK_BUTTONBOX_END - - - True - True - True - gtk-cancel - True - -6 - - - - - True - True - True - gtk-ok - True - -5 - - - 1 - - - - - False - GTK_PACK_END - - - - - - - True - DUMMY - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - - - True - DUMMY - - - False - False - 2 - - - - - - - - True - GTK_BUTTONBOX_END - - - True - True - True - gtk-cancel - True - -6 - - - - - True - True - True - gtk-ok - True - -5 - - - 1 - - - - - False - GTK_PACK_END - - - - - - - 10 - Select File - True - GTK_WIN_POS_CENTER - GDK_WINDOW_TYPE_HINT_DIALOG - True - - - True - True - True - 0 - - - - - True - True - True - 0 - - - - - Matita - - - True - - - True - - - True - GTK_SHADOW_OUT - - - True - - - True - _File - True - - - - - True - _New - True - - - - True - gtk-new - 1 - - - - - - - True - _Open... - True - - - - True - gtk-open - 1 - - - - - - - True - _Save - True - - - - True - gtk-save - 1 - - - - - - - True - Save _as ... - True - - - - True - gtk-save-as - 1 - - - - - - - - True - - - - - True - _Quit - True - - - - True - gtk-quit - 1 - - - - - - - - - - - True - _Edit - True - - - - - True - False - _Undo - True - - - - True - gtk-undo - 1 - - - - - - - True - False - _Redo - True - - - - True - gtk-redo - 1 - - - - - - - True - - - - - True - Cu_t - True - - - - True - gtk-cut - 1 - - - - - - - True - _Copy - True - - - - True - gtk-copy - 1 - - - - - - - True - _Paste - True - - - - True - gtk-paste - 1 - - - - - - - True - Paste as pattern - True - - - - - True - Paste Unicode as TeX - True - False - - - - - True - _Delete - True - - - True - gtk-delete - 1 - - - - - - - True - - - - - True - Select _All - True - - - - - True - - - - - True - _Find & replace ... - True - - - - True - gtk-find-and-replace - 1 - - - - - - - True - - - - - True - Next ligature - True - - - - - - True - Edit with e_xternal editor - True - - - - - - - - - True - _Script - True - - - - - True - Execute 1 phrase - True - - - - - - True - Retract 1 phrase - True - - - - - - True - - - - - True - Execute all - True - - - - - - True - Restart - True - - - - - - True - - - - - True - Execute until cursor - True - - - - - - - - - - True - _View - True - - - - - True - Show _tactics bar - True - True - - - - - - True - New CIC _browser - True - - - - - - True - - - - - True - _Fullscreen - True - - - - - - True - - - - - True - Zoom _in - True - - - - True - gtk-zoom-in - 1 - - - - - - - True - Zoom _out - True - - - - True - gtk-zoom-out - 1 - - - - - - - True - _Normal size - True - - - - True - gtk-zoom-100 - 1 - - - - - - - True - - - - - True - Pretty print notation - True - True - - - - - True - Hide coercions - True - True - - - - - True - - - - - True - Displays the graph of coercions - Coercions Graph - True - - - - - True - Displays a window helpful to drive automation - Auto GUI - True - - - gtk-media-pause - - - - - - - True - Displays the term grammar - Show term's grammar - True - - - - - - - - - True - _Debug - True - - - - - True - - - - - - - - - True - _Help - True - - - - - True - _Contents - True - - - - True - gtk-help - 1 - - - - - - - True - Displays the Tex/Unicode table - Show Tex/Unicode table - True - - - - - True - _About - True - - - True - gtk-about - 1 - - - - - - - - - - - - - False - False - - - - - True - - - True - True - - - True - - - True - GTK_SHADOW_OUT - GTK_POS_TOP - - - True - 17 - 2 - 4 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - True - - - - - - 15 - 16 - GTK_FILL - - - - - True - - - - - - 13 - 14 - GTK_FILL - - - - - True - - - - - - 10 - 11 - GTK_FILL - - - - - True - - - - - - 7 - 8 - GTK_FILL - - - - - True - - - - - - 5 - 6 - GTK_FILL - - - - - True - - - - - - 3 - 4 - GTK_FILL - - - - - True - - - - - - 1 - 2 - GTK_FILL - - - - - True - True - - - True - True - Split - ∧ - True - 0 - - - - - True - True - Left - L - True - 0 - - - 1 - - - - - 6 - 7 - GTK_FILL - GTK_FILL - - - - - True - True - - - True - True - Right - R - True - 0 - - - - - True - True - Exists - ∃ - True - 0 - - - 1 - - - - - 1 - 2 - 6 - 7 - GTK_FILL - GTK_FILL - - - - - True - True - ElimType - elimTy - True - 0 - - - 1 - 2 - 4 - 5 - GTK_FILL - - - - - - True - True - Replace - repl - True - 0 - - - 1 - 2 - 16 - 17 - GTK_FILL - - - - - - True - True - Cut - cut - True - 0 - - - 16 - 17 - GTK_FILL - - - - - - True - True - Auto - auto - True - 0 - - - 1 - 2 - 14 - 15 - GTK_FILL - - - - - - True - True - Assumption - assum - True - 0 - - - 14 - 15 - GTK_FILL - - - - - - True - True - Whd - whd - True - 0 - - - 12 - 13 - GTK_FILL - - - - - - True - True - Reduce - red - True - 0 - - - 1 - 2 - 11 - 12 - GTK_FILL - - - - - - True - True - Simplify - simpl - True - 0 - - - 11 - 12 - GTK_FILL - - - - - - True - True - Transitivity - trans - True - 0 - - - 9 - 10 - GTK_FILL - - - - - - True - True - Symmetry - sym - True - 0 - - - 1 - 2 - 8 - 9 - GTK_FILL - - - - - - True - True - Reflexivity - refl - True - 0 - - - 8 - 9 - GTK_FILL - - - - - - True - True - Elim - elim - True - 0 - - - 4 - 5 - GTK_FILL - - - - - - True - True - Exact - exact - True - 0 - - - 2 - 3 - GTK_FILL - - - - - - True - True - Intros - intro - True - 0 - - - GTK_FILL - - - - - - True - True - Apply - apply - True - 0 - - - 1 - 2 - GTK_FILL - - - - - - - - False - - - - - 400 - True - - - True - - - True - GTK_TOOLBAR_BOTH - - - True - - - True - True - Restart - GTK_RELIEF_NONE - 0 - - - True - gtk-goto-top - - - - - - - False - False - - - - - True - - - True - True - Retract 1 phrase - GTK_RELIEF_NONE - 0 - - - True - gtk-go-up - - - - - - - False - False - - - - - True - - - True - True - Execute until point - GTK_RELIEF_NONE - 0 - - - True - gtk-jump-to - - - - - - - False - False - - - - - True - - - True - True - Execute 1 phrase - GTK_RELIEF_NONE - 0 - - - True - gtk-go-down - - - - - - - False - False - - - - - True - - - True - True - Execute all - GTK_RELIEF_NONE - 0 - - - True - gtk-goto-bottom - - - - - - - False - False - - - - - - - True - GTK_ORIENTATION_VERTICAL - - - True - - - True - True - GTK_RELIEF_NONE - 0 - - - True - gtk-stop - - - - - - - False - False - - - - - False - 1 - - - - - False - False - - - - - True - True - GTK_POS_BOTTOM - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - - - - False - - - - - True - script - - - tab - False - False - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - True - - - True - Not implemented. - - - - - - - 1 - False - - - - - True - outline - - - tab - 1 - False - False - - - - - 1 - - - - - 1 - - - - - False - True - - - - - 250 - 500 - True - True - 380 - - - True - True - - - False - True - - - - - True - - - True - True - GTK_POLICY_NEVER - GTK_SHADOW_IN - - - True - True - False - GTK_WRAP_CHAR - False - - - - - - - True - True - - - - - True - True - - - - - - - 1 - - - - - True - - - True - False - - - - - True - False - - - True - gtk-missing-image - - - False - - - - - True - label14 - - - tab - False - False - - - - - True - gtk-missing-image - - - 1 - False - - - - - True - label15 - - - tab - 1 - False - False - - - - - True - gtk-missing-image - - - 2 - False - - - - - True - label16 - - - tab - 2 - False - False - - - - - False - 1 - - - - - False - False - 2 - - - - - - - - - DUMMY - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - - - True - DUMMY - - - False - False - 2 - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - - - True - True - - - - - 3 - - - - - True - GTK_BUTTONBOX_END - - - True - True - True - gtk-cancel - True - -6 - - - - - True - True - True - gtk-ok - True - -5 - - - 1 - - - - - False - GTK_PACK_END - - - - - - - 280 - Uri choice - True - GTK_WIN_POS_CENTER - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - 4 - - - True - 3 - - - True - some informative message here ... - - - False - False - - - - - 400 - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - - - True - True - False - - - - - 1 - - - - - True - - - True - URI: - - - False - False - - - - - True - True - * - - - 1 - - - - - False - 2 - - - - - 2 - - - - - True - GTK_BUTTONBOX_END - - - True - True - True - gtk-cancel - True - -6 - - - - - True - True - True - 0 - - - True - 0 - 0 - - - True - 2 - - - True - gtk-index - - - False - False - - - - - True - Try _Selected - True - - - False - False - 1 - - - - - - - - - 1 - - - - - True - False - True - True - Try Constants - True - 0 - - - 2 - - - - - True - True - gtk-copy - True - 0 - - - 3 - - - - - True - True - True - 0 - - - True - 0 - 0 - - - True - 2 - - - True - gtk-ok - - - False - False - - - - - True - bla bla bla - True - - - False - False - 1 - - - - - - - - - 4 - - - - - True - True - True - gtk-go-forward - True - 0 - - - 5 - - - - - False - GTK_PACK_END - - - - - - - 5 - Find & Replace - False - GTK_WIN_POS_MOUSE - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - 3 - 2 - 5 - - - True - 5 - - - True - - - - - - - - - - - True - True - gtk-find - True - 0 - - - False - False - 1 - - - - - True - True - 0 - - - True - 0 - 0 - - - True - 2 - - - True - gtk-find-and-replace - - - False - False - - - - - True - _Replace - True - - - False - False - 1 - - - - - - - - - False - False - 2 - - - - - True - True - gtk-cancel - True - 0 - - - False - False - 3 - - - - - 2 - 2 - 3 - 5 - - - - - True - True - * - - - 1 - 2 - 1 - 2 - - - - - - True - True - True - True - True - * - - - 1 - 2 - - - - - - True - 0 - Replace with: - - - 1 - 2 - GTK_FILL - - - - - - True - 0 - Find: - - - GTK_FILL - - - - - - - - 450 - 400 - title - True - GDK_WINDOW_TYPE_HINT_DIALOG - - - True - - - True - - - True - some informative message here ... - - - False - False - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - - - True - True - False - - - - - 1 - - - - - 2 - - - - - True - GTK_BUTTONBOX_END - - - True - True - True - gtk-help - True - -11 - - - - - True - True - True - -6 - - - True - 0 - 0 - - - True - 2 - - - True - gtk-zoom-in - - - False - False - - - - - True - More - True - - - False - False - 1 - - - - - - - - - 1 - - - - - True - True - True - True - gtk-cancel - True - -6 - - - 2 - - - - - True - True - True - gtk-ok - True - -5 - - - 3 - - - - - False - GTK_PACK_END - - - - - - - 600 - 400 - True - Auto - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_SOUTH_EAST - - - True - - - True - 2 - - - True - True - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - - - True - - - True - 3 - 3 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - True - - - True - True - 0 - - - True - 0 - 0 - - - True - 2 - - - True - gtk-go-up - - - False - False - - - - - True - True - - - False - False - 1 - - - - - - - - - - - True - True - 0 - - - True - gtk-go-down - - - - - 1 - - - - - False - False - 1 - - - - - - - True - - - False - 3 - 1 - - - - - True - - - True - 0 - Last: - - - - - True - 4 - 4 - GTK_BUTTONBOX_END - - - True - True - True - gtk-media-pause - True - 0 - - - - - True - True - True - gtk-media-play - True - 0 - - - 1 - - - - - True - True - True - gtk-media-next - True - 0 - - - 2 - - - - - True - True - True - gtk-close - True - 0 - - - 3 - - - - - 1 - - - - - False - 2 - - - - - + + + True + Cic browser + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER_ON_PARENT + False + 500 + 500 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + True + False + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_PACK_DIRECTION_LTR + GTK_PACK_DIRECTION_LTR + + + + True + _File + True + + + + + + + True + gtk-new + True + + + + + + True + Open _Location ... + True + + + + + + + True + + + + + + True + gtk-close + True + + + + + + + + + + True + _Edit + True + + + + + + + True + gtk-copy + True + + + + + + + + + + True + _View + True + + + + + + + True + _Metadata + True + + + + + + True + View the graph of objects on which the current one depends on + (Direct) Dependencies + True + + + + + + True + View the graph of objects which depends on the current one + (Inverse) Dependencies + True + + + + + + True + + + + + + True + HBugs Tutors + True + + + + + + + + + 0 + False + False + + + + + + True + 0 + 0 + GTK_SHADOW_NONE + + + + True + False + 0 + + + + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + refresh + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-refresh + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + home + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-home + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + gtk-jump-to + 2 + 0.5 + 0.5 + 0 + 0 + + + 3 + False + False + + + + + + True + False + 0 + + + + + + + 0 + True + True + + + + + + + 0 + False + True + + + + + + 3 + True + False + 6 + + + + True + gtk-missing-image + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + True + + + + + + True + True + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + + True + False + 0 + + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + + + + + 0 + False + False + + + + + 0 + False + True + + + + + 0 + False + True + + + + + + True + True + True + True + GTK_POS_TOP + False + False + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + False + True + + + + + + True + MathView + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + False + False + False + + + + + False + True + + + + + + True + WhelpResults + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + GTK_SHADOW_NONE + + + + True + gtk-missing-image + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + True + + + + + + True + WhelpEasterEgg + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + False + True + + + + + + True + Graph + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + False + 0 + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + False + False + False + + + + + 0 + True + True + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + True + gtk-refresh + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + True + gtk-remove + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + True + gtk-add + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + False + True + + + + + + True + HBugs + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + 0 + True + True + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + True + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + + + + 10 + Select File + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + + + Matita + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + True + False + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP + + + + True + GTK_PACK_DIRECTION_LTR + GTK_PACK_DIRECTION_LTR + + + + True + _File + True + + + + + + + True + _New + True + + + + + True + gtk-new + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Open... + True + + + + + True + gtk-open + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Save + True + + + + + True + gtk-save + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Save _as ... + True + + + + + True + gtk-save-as + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + _Quit + True + + + + + True + gtk-quit + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + + + + True + _Edit + True + + + + + + + True + False + _Undo + True + + + + + True + gtk-undo + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + False + _Redo + True + + + + + True + gtk-redo + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + Cu_t + True + + + + + True + gtk-cut + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Copy + True + + + + + True + gtk-copy + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Paste + True + + + + + True + gtk-paste + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Paste as pattern + True + + + + + + True + Paste Unicode as TeX + True + False + + + + + + True + _Delete + True + + + + True + gtk-delete + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + Select _All + True + + + + + + True + + + + + + True + _Find & replace ... + True + + + + + True + gtk-find-and-replace + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + Next ligature + True + + + + + + + True + Edit with e_xternal editor + True + + + + + + + + + + True + _Script + True + + + + + + + True + Execute 1 phrase + True + + + + + + + True + Retract 1 phrase + True + + + + + + + True + + + + + + True + Execute all + True + + + + + + + True + Restart + True + + + + + + + True + + + + + + True + Execute until cursor + True + + + + + + + + + + + True + _View + True + + + + + + + True + Show _tactics bar + True + True + + + + + + + True + New CIC _browser + True + + + + + + + True + + + + + + True + _Fullscreen + True + False + + + + + + + True + + + + + + True + Zoom _in + True + + + + + True + gtk-zoom-in + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Zoom _out + True + + + + + True + gtk-zoom-out + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Normal size + True + + + + + True + gtk-zoom-100 + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + Pretty print notation + True + True + + + + + + True + Hide coercions + True + True + + + + + + True + + + + + + True + Displays the graph of coercions + Coercions Graph + True + + + + + + True + Displays a window helpful to drive automation + Auto GUI + True + + + + gtk-media-pause + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Displays the term grammar + Show term's grammar + True + + + + + + + + + + True + _Debug + True + + + + + + + True + + + + + + + + + + True + _Help + True + + + + + + + True + _Contents + True + + + + + True + gtk-help + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Displays the Tex/Unicode table + Show Tex/Unicode table + True + + + + + + True + _About + True + + + + True + gtk-about + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + + + + + 0 + False + False + + + + + + True + False + 0 + + + + True + True + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_TOP + GTK_POS_TOP + + + + True + False + 0 + + + + + + + + + + + + + + + + + 0 + False + True + + + + + + 400 + True + False + 0 + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Restart + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Retract 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute until point + True + GTK_RELIEF_NONE + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute all + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + 0 + True + True + + + + + + True + GTK_ORIENTATION_VERTICAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-stop + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + 0 + False + True + + + + + 0 + False + False + + + + + + True + True + True + True + GTK_POS_BOTTOM + False + False + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + False + True + + + + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + GTK_SHADOW_IN + + + + True + Not implemented. + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + + + + + False + True + + + + + + True + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + 0 + True + True + + + + + 0 + True + True + + + + + True + False + + + + + + 250 + 500 + True + True + 380 + + + + True + True + True + True + GTK_POS_TOP + False + False + + + True + False + + + + + + True + False + 0 + + + + True + True + GTK_POLICY_NEVER + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_CHAR + False + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + True + True + + + + + True + True + + + + + 0 + True + True + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + False + + + 0 + True + True + + + + + + True + False + True + GTK_POS_TOP + False + False + + + + True + gtk-missing-image + 4 + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label14 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + gtk-missing-image + 4 + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label15 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + + True + gtk-missing-image + 4 + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label16 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + + + + 0 + False + True + + + + + 0 + False + False + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + + + + 280 + Uri choice + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + False + 4 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-index + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Try _Selected + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + + + + True + False + True + True + Try Constants + True + GTK_RELIEF_NORMAL + True + 0 + + + + + + True + True + gtk-copy + True + GTK_RELIEF_NORMAL + True + 0 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-ok + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + bla bla bla + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + + + + True + True + True + gtk-go-forward + True + GTK_RELIEF_NORMAL + True + 0 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 3 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + 400 + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + False + False + False + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + URI: + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + True + True + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + 0 + False + True + + + + + 0 + True + True + + + + + + + + 5 + Find & Replace + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_MOUSE + False + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + + + + True + 3 + 2 + False + 5 + 0 + + + + True + False + 5 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + gtk-find + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-find-and-replace + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + _Replace + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + 0 + 2 + 2 + 3 + 5 + + + + + + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 1 + 2 + + + + + + + True + True + True + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 0 + 1 + + + + + + + True + Replace with: + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + 1 + 1 + 2 + + + + + + + + True + Find: + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + 1 + 0 + 1 + + + + + + + + + + 450 + 400 + title + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-help + True + GTK_RELIEF_NORMAL + True + -11 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + -6 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-zoom-in + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + More + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + + + + True + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + False + False + False + + + + + 0 + True + True + + + + + 0 + True + True + + + + + + + + 600 + 400 + True + Auto + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_SOUTH_EAST + True + False + + + + True + False + 0 + + + + True + False + 2 + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + GTK_SHADOW_IN + + + + True + 3 + 3 + False + 0 + 0 + + + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + 0 + True + True + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + True + True + + + + + 0 + False + False + + + + + 0 + True + True + + + + + + True + + + 3 + False + True + + + + + + True + False + 0 + + + + True + Last: + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + True + True + + + + + + 4 + True + GTK_BUTTONBOX_END + 4 + + + + True + True + True + gtk-media-pause + True + GTK_RELIEF_NORMAL + True + + + + + + True + True + True + gtk-media-play + True + GTK_RELIEF_NORMAL + True + + + + + + True + True + True + gtk-media-next + True + GTK_RELIEF_NORMAL + True + + + + + + True + True + True + gtk-close + True + GTK_RELIEF_NORMAL + True + + + + + 0 + True + True + + + + + 0 + False + True + + + + + + + + True + SearchWin + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER_ON_PARENT + False + 640 + 480 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_CENTER + True + False + + + + True + False + 0 + + + + 4 + True + False + 4 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + True + True + 0 + + True + ● + False + + + 0 + True + True + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-find + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Search + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + 0 + False + True + + + + + + 3 + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + + + + 0 + True + True + + + + + + True + + + 4 + False + True + + + + + + 4 + True + False + 0 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-close + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Close + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + 0 + False + False + + + + + + + + + 0 + False + True + + + + + 0 + False + True + + + + + + diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index 9c00dfdde..fa0c4a334 100644 --- a/helm/software/matita/matitaGtkMisc.ml +++ b/helm/software/matita/matitaGtkMisc.ml @@ -412,3 +412,29 @@ let utf8_string_length s = assert(Glib.Utf8.validate s); Glib.Utf8.length s +let new_search_win title text = + let w = new MatitaGeneratedGui.searchWin () in + let t = + GSourceView.source_view ~auto_indent:false ~editable:false () + in + t#source_buffer#insert text; + w#toplevel#set_title title; + w#scrolledwinContent#add (t :> GObj.widget); + ignore(w#buttonSearch#connect#clicked ~callback:( fun () -> + let text = w#entrySearch#text in + let highlight start end_ = + t#source_buffer#move_mark `INSERT ~where:start; + t#source_buffer#move_mark `SEL_BOUND ~where:end_; + t#scroll_mark_onscreen `INSERT + in + let iter = t#source_buffer#get_iter `SEL_BOUND in + match iter#forward_search text with + | None -> + (match t#source_buffer#start_iter#forward_search text with + | None -> () + | Some (start,end_) -> highlight start end_) + | Some (start,end_) -> highlight start end_)); + ignore(w#buttonClose#connect#clicked ~callback:(fun () -> + w#toplevel#misc#hide (); w#toplevel#destroy ())); + w +;; diff --git a/helm/software/matita/matitaGtkMisc.mli b/helm/software/matita/matitaGtkMisc.mli index 0f78a4a61..03d89cd27 100644 --- a/helm/software/matita/matitaGtkMisc.mli +++ b/helm/software/matita/matitaGtkMisc.mli @@ -151,4 +151,4 @@ val utf8_parsed_text: string -> Stdpp.location -> string * int (* the length in characters, not bytes *) val utf8_string_length: string -> int - +val new_search_win: string -> string -> MatitaGeneratedGui.searchWin diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 55b044ba4..5d9d87c86 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -907,31 +907,18 @@ class gui () = (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); connect_menu_item main#showTermGrammarMenuItem (fun _ -> - let w = GWindow.window ~resizable:true - ~position:`CENTER_ON_PARENT - ~title:"Terms grammar" ~width:640 ~height:400 () in - w#set_transient_for (main#toplevel#as_window); - let s = GBin.scrolled_window () in - (w :> GContainer.container)#add (s :> GObj.widget); - let t = GText.view () in - t#buffer#insert (Print_grammar.ebnf_of_term ()); - s#add (t:>GObj.widget); - w#show ()); + let w = MatitaGtkMisc.new_search_win "Terms grammar" (Print_grammar.ebnf_of_term ()) in + w#toplevel#set_transient_for (main#toplevel#as_window); + w#toplevel#show ()); connect_menu_item main#showUnicodeTable (fun _ -> - let w = GWindow.window ~resizable:true - ~position:`CENTER_ON_PARENT - ~title:"Tex/UTF8 table" ~width:640 ~height:400 () in - w#set_transient_for (main#toplevel#as_window); - let s = GBin.scrolled_window () in - (w :> GContainer.container)#add (s :> GObj.widget); - let t = GTree.view () in - let m = new MatitaGtkMisc.multiStringListModel ~cols:2 t in - List.iter (fun (k,vs) -> - m#easy_mappend [k;String.concat " " vs]) - (Utf8Macro.pp_table ()); - s#add (t:>GObj.widget); - w#show ()); + let text = String.concat "\n" + (List.map (fun (k,vs) -> "\t" ^ k ^ "\t" ^ String.concat ", " vs) + (Utf8Macro.pp_table ())) + in + let w = MatitaGtkMisc.new_search_win "Tex/UTF8 table" text in + w#toplevel#set_transient_for (main#toplevel#as_window); + w#toplevel#show ()); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) -- 2.39.2