X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=0d80fe22c933960827789de606e3c3601b392610;hb=11a22c74b3b2307eedf89c0439ba02d199dcdc9e;hp=72ba3db8c62fcfb806e7c1bd0c601aa5930d7397;hpb=9d2f0cf4764f3fe9c85bcb8f6b06a426d99cfa44;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 72ba3db8c..0d80fe22c 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -3,11 +3,14 @@ + 500 + 480 True Cic browser GTK_WIN_POS_CENTER_ON_PARENT 500 - 500 + 480 + True True @@ -83,13 +86,6 @@ True - - - True - _Metadata - True - - True @@ -107,8 +103,10 @@ - + True + Universes + True @@ -332,9 +330,6 @@ - - False - @@ -343,7 +338,6 @@ tab - False False @@ -364,7 +358,6 @@ 1 - False @@ -375,7 +368,6 @@ tab 1 - False False @@ -400,7 +392,6 @@ 2 - False @@ -411,7 +402,6 @@ tab 2 - False False @@ -427,7 +417,6 @@ 3 - False @@ -438,7 +427,6 @@ tab 3 - False False @@ -525,7 +513,6 @@ 4 - False @@ -536,7 +523,145 @@ tab 4 - False + False + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + + + True + True + + + + + 5 + + + + + True + Universes + + + tab + 5 + False + + + + + True + + + True + True + 3 + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + + + + + + + + True + 4 + 4 + + + True + + + + + + + + + + + True + True + True + + + 1 + + + + + True + True + 0 + + + True + 0 + 0 + + + True + 2 + + + True + gtk-find + + + False + False + + + + + True + Search + True + + + False + False + 1 + + + + + + + + + False + False + 2 + + + + + False + 1 + + + + + 6 + + + + + True + SearchText + + + tab + 6 False @@ -770,21 +895,6 @@ - - - True - _Developments... - True - - - - True - gtk-execute - 1 - - - - True @@ -910,7 +1020,15 @@ True Paste Unicode as TeX True - False + + + + + True + Automatically expands TeX macros to their corresponding UTF-8 symbol + Auto-expand TeX Macros + True + True @@ -1051,15 +1169,6 @@ True - - - True - Show _tactics bar - True - True - - - True @@ -1081,6 +1190,15 @@ + + + True + Shows a palette with natural deduction rules + Natural deduction palette + True + + + True @@ -1165,6 +1283,14 @@ True + + + True + Displays the database of hints + Hints database + True + + True @@ -1178,6 +1304,28 @@ + + + True + Displays the terms grammar as extended by the user + Terms grammar + True + + + + + True + Show the conversion table from TeX like sequences to UTF-8 + TeX/UTF-8 table + True + + + True + gtk-select-font + + + + @@ -1247,7 +1395,7 @@ - + True @@ -1256,623 +1404,336 @@ True + 2 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 - 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 + True 0 - + True - gtk-goto-top + Implication (⇒<sub>i</sub>) + True - - - False - False - - - - - True - + True True - Retract 1 phrase - GTK_RELIEF_NONE + True 0 - + True - gtk-go-up + Conjunction (∧<sub>i</sub>) + True + + 1 + - - - False - False - - - - - True - + True True - Execute until point - GTK_RELIEF_NONE + True 0 - + True - gtk-jump-to + Disjunction left (∨<sub>i-l</sub>) + True + + 2 + - - - False - False - - - - - True - + True True - Execute 1 phrase - GTK_RELIEF_NONE + True 0 - + True - gtk-go-down + Disjunction right (∨<sub>i-r</sub>) + True + + 3 + - - - False - False - - - - - True - + True True - Execute all - GTK_RELIEF_NONE + True 0 - + True - gtk-goto-bottom + Negation (¬<sub>i</sub>) + True + + + + + 4 + + + + + True + True + True + 0 + + + True + Top (⊤<sub>i</sub>) + True + + + + + 5 + + + + + True + True + True + 0 + + + True + Universal (∀<sub>i</sub>) + True + + + + + 6 + + + + + True + True + True + 0 + + + True + Existential (∃<sub>i</sub>) + True + + 7 + + + + + True + Introduction rules + - False - False + label_item + + False + - + True - GTK_ORIENTATION_VERTICAL + True - + True - + True True - GTK_RELIEF_NONE + True 0 - + True - gtk-stop + Implication (⇒<sub>e</sub>) + True - - - False - False + + + True + True + True + 0 + + + True + Conjunction left (∧<sub>e-l</sub>) + True + + + + + 1 + + + + + True + True + True + 0 + + + True + Conjunction right (∧<sub>e-r</sub>) + True + + + + + 2 + + + + + True + True + True + 0 + + + True + Disjunction (∨<sub>e</sub>) + True + + + + + 3 + + + + + True + True + True + 0 + + + True + Negation (¬<sub>e</sub>) + True + + + + + 4 + + + + + True + True + True + 0 + + + True + Bottom (⊥<sub>e</sub>) + True + + + + + 5 + + + + + True + True + True + 0 + + + True + Universal (∀<sub>e</sub>) + True + + + + + 6 + + + + + True + True + True + 0 + + + True + Existential (∃<sub>e</sub>) + True + + + + + 7 + + + + + + + True + Elimination rules + + + label_item @@ -1881,626 +1742,448 @@ 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. + True + True + Reduction to Absurdity (RAA) + 0 + + + + + True + True + True + Use lemma (lem) + 0 + + + 1 + + + + + True + True + True + Discharge (discharge) + 0 + + 2 + + + + True + Misc rules + + + label_item + + - 1 - False - - - - - True - outline - - - tab - 1 - False - False + False + 2 - - 1 - - 1 - - - - - False - True - - - - - 250 - 500 - True - True - 380 - - - True - True - - - False - True + False - + + 400 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 + 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 + GTK_TOOLBAR_BOTH + + + 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 + + + + + + + + True + script + + + tab + False + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + + + True + + + True + Not implemented. + + + + + + + 1 + + + + + True + outline + + + tab + 1 + False + + + + + 1 + + - False - False 1 + + False + True + - - - - - 1 - - - - - True - False - True - True - Try Constants - True - 0 - - - 2 - - - - - True - True - gtk-copy - True - 0 - - - 3 - - - - - True - True - True - 0 - - - True - 0 - 0 - + + 250 + 500 True - 2 + True + 380 - + True - gtk-ok + True - False - False + False + True - + True - bla bla bla - True + + + True + True + GTK_POLICY_NEVER + GTK_SHADOW_IN + + + True + True + False + GTK_WRAP_CHAR + False + + + + - False - False - 1 + True + True + + True + True + - 4 - - - - - True - True - True - gtk-go-forward - True - 0 - - - 5 + 1 - - - 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 + False + - - - - - True - True - gtk-find - True - 0 - - - False - False - 1 - - - - - True - True - 0 - + True - 0 - 0 + False + + + True + gtk-missing-image + + + + + True + label14 + + + tab + False + + + + + True + gtk-missing-image + + + 1 + + + + + True + label15 + + + tab + 1 + False + + - + True - 2 - - - True - gtk-find-and-replace - - - False - False - - - - - True - _Replace - True - - - False - False - 1 - - + gtk-missing-image + + 2 + + + + + True + label16 + + + tab + 2 + False + + + False + 1 + @@ -2509,333 +2192,192 @@ 2 - - - True - True - gtk-cancel - True - 0 - - - False - False - 3 - - - - 2 - 2 - 3 - 5 - + + + + + DUMMY + GDK_WINDOW_TYPE_HINT_DIALOG + + + True - + True - True - * + DUMMY - 1 - 2 - 1 - 2 - + False + False + 2 - + True True - True - True - True - * - - - 1 - 2 - - - - - - True - 0 - Replace with: - - - 1 - 2 - GTK_FILL - - - - - - True - 0 - Find: - - - GTK_FILL - - - - - - - - Create development - False - True - GTK_WIN_POS_CENTER_ALWAYS - GDK_WINDOW_TYPE_HINT_UTILITY - - - True - - - True - 3 - 2 - 3 - 5 - 5 - - - - - - True - True - ... - True - 0 - - - 2 - 3 - 1 - 2 - GTK_FILL - - - - - - True - True - * - - - 1 - 2 - 1 - 2 - - - + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN - + True True - * - - - 1 - 2 - - - - - - True - 0 - Root directory - - - 1 - 2 - GTK_FILL - - - - - - True - 0 - Name - - GTK_FILL - - - False - - - - - True - - - False - 2 - 1 + 3 - - + + True - 3 - 5 - - - True - - - - - - - - + GTK_BUTTONBOX_END - + True True - gtk-add + True + gtk-cancel True - 0 + -6 - - False - False - 1 - - + True True - gtk-cancel + True + gtk-ok True - 0 + -5 - False - False - 2 + 1 False - 2 + GTK_PACK_END - - Developments + + 280 + Uri choice + True GTK_WIN_POS_CENTER - - + GDK_WINDOW_TYPE_HINT_DIALOG + + True + 4 - + True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN + 3 - + True - True - False + some informative message here ... + + False + False + - - - - - True - - - False - 2 - 1 - - - - - True - 3 - 4 - + + 400 True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC - - - - + + True + True + False + + + 1 + - + True - True - gtk-new - True - 0 + + + True + URI: + + + False + False + + + + + True + True + * + + + 1 + + False - False - 1 + 2 + + + 2 + + + + + True + GTK_BUTTONBOX_END - + True True - gtk-delete + True + gtk-cancel True - 0 + -6 - - False - False - 2 - - + True True + True 0 - + True 0 0 - + True 2 - + True - gtk-execute + gtk-index False @@ -2843,9 +2385,9 @@ - + True - _Build + Try _Selected True @@ -2860,29 +2402,54 @@ - False - False + 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-clear + gtk-ok False @@ -2890,9 +2457,9 @@ - + True - C_lean + bla bla bla True @@ -2907,76 +2474,143 @@ - False - False 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 + 0 + Find: + + + + + + + + + True + 0 + Replace with: + + + 1 + 2 + + + + + + + True + True + True + True + True + * + + + 1 + 2 + + + + + + True + True + * + + + 1 + 2 + 1 + 2 + + + + + + True + 5 + + + True - - True - 0 - 0 - - - True - 2 - - - True - gtk-convert - - - False - False - - - - - True - Publish - True - - - False - False - 1 - - - - - + + + + + + + + True + True + gtk-find + True + 0 + False False - 5 + 1 - + True True 0 - + True 0 0 - + True 2 - + True - gtk-zoom-fit + gtk-find-and-replace False @@ -2984,9 +2618,9 @@ - + True - Graph + _Replace True @@ -3003,27 +2637,29 @@ False False - 6 + 2 - + True True - gtk-close + gtk-cancel True 0 False False - 7 + 3 - False - 2 + 2 + 2 + 3 + 5