From 6ff514ec3bdc39bd0afbdfb210290a670a20a60d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jul 2007 10:46:11 +0000 Subject: [PATCH] fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions --- matita/lablGraphviz.ml | 5 +- matita/matita.glade | 8371 +++++++++++++++---------------------- matita/matitaGui.ml | 6 + matita/tests/coercions.ma | 17 + matita/tests/overred.ma | 33 + 5 files changed, 3451 insertions(+), 4981 deletions(-) create mode 100644 matita/tests/overred.ma diff --git a/matita/lablGraphviz.ml b/matita/lablGraphviz.ml index 27e7d4b9a..d86d943e3 100644 --- a/matita/lablGraphviz.ml +++ b/matita/lablGraphviz.ml @@ -86,13 +86,16 @@ class graphviz_impl ?packing () = method private load_map fname = let areas = ref [] in + let is_rect l = + try List.assoc "shape" l = "rect" with Not_found -> false + in let p = XmlPushParser.create_parser { XmlPushParser.default_callbacks with XmlPushParser.start_element = Some (fun elt attrs -> match elt with - | "area" -> areas := attrs :: !areas + | "area" when is_rect attrs -> areas := attrs :: !areas | _ -> ()) } in XmlPushParser.parse p (`File fname); map <- !areas diff --git a/matita/matita.glade b/matita/matita.glade index 81a68b55d..31ca67c33 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -1,4982 +1,3393 @@ - - - + + + - - - 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 - 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 - 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 - _Developments... - True - - - - - True - gtk-execute - 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 - True - - - - - - 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 - _Debug - True - - - - - - - True - - - - - - - - - - True - _Help - True - - - - - - - True - _Contents - True - - - - - True - gtk-help - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - 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 - 17 - 2 - False - 4 - 0 - - - - True - Apply - True - apply - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 0 - 1 - fill - - - - - - - True - Intros - True - intro - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 0 - 1 - fill - - - - - - - True - Exact - True - exact - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 2 - 3 - fill - - - - - - - True - Elim - True - elim - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 4 - 5 - fill - - - - - - - True - Reflexivity - True - refl - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 8 - 9 - fill - - - - - - - True - Symmetry - True - sym - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 8 - 9 - fill - - - - - - - True - Transitivity - True - trans - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 9 - 10 - fill - - - - - - - True - Simplify - True - simpl - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 11 - 12 - fill - - - - - - - True - Reduce - True - red - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 11 - 12 - fill - - - - - - - True - Whd - True - whd - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 12 - 13 - fill - - - - - - - True - Assumption - True - assum - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 14 - 15 - fill - - - - - - - True - Auto - True - auto - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 14 - 15 - fill - - - - - - - True - Cut - True - cut - True - GTK_RELIEF_NORMAL - True - - - 0 - 1 - 16 - 17 - fill - - - - - - - True - Replace - True - repl - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 16 - 17 - fill - - - - - - - True - ElimType - True - elimTy - True - GTK_RELIEF_NORMAL - True - - - 1 - 2 - 4 - 5 - fill - - - - - - - True - True - 0 - - - - True - Right - True - R - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - - True - Exists - True - ∃ - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - 1 - 2 - 6 - 7 - fill - fill - - - - - - True - True - 0 - - - - True - Split - True - ∧ - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - - True - Left - True - L - True - GTK_RELIEF_NORMAL - True - - - 0 - True - True - - - - - 0 - 1 - 6 - 7 - fill - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 1 - 2 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 3 - 4 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 5 - 6 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 7 - 8 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 10 - 11 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 13 - 14 - fill - - - - - - True - 0.5 - 0.5 - 1 - 1 - 0 - 0 - 0 - 0 - - - - - - - 0 - 1 - 15 - 16 - fill - - - - - - - 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_ICONS - 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 - 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 - 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 - 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 - Find: - False - False - GTK_JUSTIFY_LEFT - False - False - 0 - 0.5 - 0 - 0 - PANGO_ELLIPSIZE_NONE - -1 - False - 0 - - - 0 - 1 - 0 - 1 - fill - - - - - - - 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 - fill - - - - - - - True - True - True - True - True - True - True - 0 - - True - * - False - - - 1 - 2 - 0 - 1 - - - - - - - True - True - True - True - 0 - - True - * - False - - - 1 - 2 - 1 - 2 - - - - - - - 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 - - - - - - - - Create development - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER_ALWAYS - True - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_UTILITY - GDK_GRAVITY_NORTH_WEST - True - False - - - - True - False - 0 - - - - 3 - True - 2 - 3 - False - 5 - 5 - - - - True - Name - False - False - GTK_JUSTIFY_LEFT - False - False - 0 - 0.5 - 0 - 0 - PANGO_ELLIPSIZE_NONE - -1 - False - 0 - - - 0 - 1 - 0 - 1 - fill - - - - - - - True - Root directory - False - False - GTK_JUSTIFY_LEFT - False - False - 0 - 0.5 - 0 - 0 - PANGO_ELLIPSIZE_NONE - -1 - False - 0 - - - 0 - 1 - 1 - 2 - fill - - - - - - - True - True - True - True - 0 - - True - * - False - - - 1 - 2 - 0 - 1 - - - - - - - True - True - True - True - 0 - - True - * - False - - - 1 - 2 - 1 - 2 - - - - - - - True - True - ... - True - GTK_RELIEF_NORMAL - True - - - 2 - 3 - 1 - 2 - fill - - - - - - 0 - False - True - - - - - - True - - - 2 - False - True - - - - - - 3 - True - False - 5 - - - - True - False - 0 - - - - - - - - - - - 0 - True - True - - - - - - True - True - gtk-add - True - GTK_RELIEF_NORMAL - True - - - 0 - False - False - - - - - - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - - - 0 - False - False - - - - - 0 - False - True - - - - - - - - Developments - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - True - False - - - - True - False - 0 - - - - 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 - - - - - - True - - - 2 - False - True - - - - - - 3 - True - False - 4 - - - - True - False - 0 - - - - - - - - - - - 0 - True - True - - - - - - True - True - gtk-new - True - GTK_RELIEF_NORMAL - True - - - 0 - False - False - - - - - - True - True - gtk-delete - 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-execute - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - _Build - 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_RELIEF_NORMAL - True - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-clear - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - C_lean - 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_RELIEF_NORMAL - True - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-convert - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - Publish - 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_RELIEF_NORMAL - True - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-zoom-fit - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - Graph - 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-close - True - GTK_RELIEF_NORMAL - True - - - 0 - False - False - - - - - 0 - False - True - - - - - - - - 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 + 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 + _Developments... + True + + + + True + gtk-execute + 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 + True + + + + + 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 + Coericons Graph + True + + + + + True + Displays a window helpful to drive automation + Auto GUI + True + + + gtk-media-pause + + + + + + + + + + + True + _Debug + True + + + + + True + + + + + + + + + True + _Help + True + + + + + True + _Contents + True + + + + True + gtk-help + 1 + + + + + + + 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 + + + + + + + + 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 + + + + + + True + True + * + + + 1 + 2 + + + + + + True + 0 + Root directory + + + 1 + 2 + GTK_FILL + + + + + + True + 0 + Name + + + GTK_FILL + + + + + + False + + + + + True + + + False + 2 + 1 + + + + + True + 3 + 5 + + + True + + + + + + + + + + + True + True + gtk-add + True + 0 + + + False + False + 1 + + + + + True + True + gtk-cancel + True + 0 + + + False + False + 2 + + + + + False + 2 + + + + + + + Developments + GTK_WIN_POS_CENTER + + + True + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + + + True + True + False + + + + + + + True + + + False + 2 + 1 + + + + + True + 3 + 4 + + + True + + + + + + + + + + + True + True + gtk-new + True + 0 + + + False + False + 1 + + + + + True + True + gtk-delete + True + 0 + + + False + False + 2 + + + + + True + True + 0 + + + True + 0 + 0 + + + True + 2 + + + True + gtk-execute + + + False + False + + + + + True + _Build + True + + + False + False + 1 + + + + + + + + + False + False + 3 + + + + + True + True + 0 + + + True + 0 + 0 + + + True + 2 + + + True + gtk-clear + + + False + False + + + + + True + C_lean + True + + + False + False + 1 + + + + + + + + + False + False + 4 + + + + + True + True + 0 + + + True + 0 + 0 + + + True + 2 + + + True + gtk-convert + + + False + False + + + + + True + Publish + True + + + False + False + 1 + + + + + + + + + False + False + 5 + + + + + True + True + 0 + + + True + 0 + 0 + + + True + 2 + + + True + gtk-zoom-fit + + + False + False + + + + + True + Graph + True + + + False + False + 1 + + + + + + + + + False + False + 6 + + + + + True + True + gtk-close + True + 0 + + + False + False + 7 + + + + + False + 2 + + + + + + + 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 + + + + + diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index f032831cb..94cb736b8 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -1173,6 +1173,12 @@ class gui () = connect_menu_item main#saveMenuItem saveScript; connect_menu_item main#saveAsMenuItem saveAsScript; connect_menu_item main#newMenuItem newScript; + connect_menu_item main#showCoercionsGraphMenuItem + (fun _ -> + let c = MatitaMathView.cicBrowser () in + c#load (`About `Coercions)); + connect_menu_item main#showAutoGuiMenuItem + (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma index 8e7582a14..3d788a813 100644 --- a/matita/tests/coercions.ma +++ b/matita/tests/coercions.ma @@ -112,6 +112,23 @@ definition mapmult: \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \d \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat. l (m m) o (o o o). +axiom T0 : Type. +axiom T1 : Type. +axiom T2 : Type. +axiom T3 : Type. + +axiom c1 : T0 -> T1. +axiom c2 : T1 -> T2. +axiom c3 : T2 -> T3. +axiom c4 : T2 -> T1. + +coercion cic:/matita/tests/coercions/c1.con. +coercion cic:/matita/tests/coercions/c2.con. +coercion cic:/matita/tests/coercions/c3.con. +coercion cic:/matita/tests/coercions/c4.con. + + + \ No newline at end of file diff --git a/matita/tests/overred.ma b/matita/tests/overred.ma new file mode 100644 index 000000000..2034001bd --- /dev/null +++ b/matita/tests/overred.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/overred/". + +include "logic/equality.ma". + +axiom T1 : Type. +axiom X : Type. +axiom x : X. +definition T2 : Type := T1. +definition T3 : Type := T2. +axiom t3 : T3. +axiom c : T2 -> X -> X. + +coercion cic:/matita/test/overred/c.con 1. + +axiom daemon : c t3 x = x. + +theorem find_a_coercion_from_T2_for_a_term_in_T3 : (* c *) t3 x = x. +apply daemon. +qed. \ No newline at end of file -- 2.39.2