[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

8. Miscellaneous Emacs facilities for fast mizaring


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

8.1 Imenu and Speedbar support

When your article becomes large, it starts to be difficult to look up in it various definitions, theorems and other items. One solution is to use the Hide/Show commands, See section Hide/Show - Hiding proofs, to hide the proofs that you do not need to see.

The Imenu and Speedbar facilities on the other hand simulate tag-like methods, generating index of important items in the edited buffer on demand. The index is then accessible either from menu, or from the special Speedbar frame. See Imenu: (emacs)Imenu, and See Speedbar: (emacs)Speedbar for more on these facilities.

In Mizar Mode, Imenu is now instructed to include into the index the following items from Mizar articles:


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

8.2 Abbreviations

Emacs can support automatic expansion of abbreviations as you type, See Abbrevs: (emacs)Abbrevs.

You can use them to make shortcuts for the long strings that you will write often in Mizar Mode - e.g. “theorem”, “correctness”, “definition”, etc.

Below are some found useful by author, you can copy them to your ‘.abbrev_defs’ file. The up-to-date version of an example ‘.abbrev_defs’ file is downloadable from the Mizar Mode CVS at http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/. You can add more abbreviations by running C-x a l (add-mode-abbrev).

Finally, if you are too lazy to define your own abbreviations, Emacs also provides “dynamic” completion by running M-/ (dabbrev-expand), See Dynamic Abbrevs: (emacs)Dynamic Abbrevs.

 
(define-abbrev-table 'mizar-mode-abbrev-table '(
    ("contra" "contradiction" nil 0)
    ("refl" "reflexivity" nil 0)
    ("hn" "hence" nil 0)
    ("hl" "holds" nil 0)
    ("pf" "proof" nil 0)
    ("cons" "consider" nil 0)
    ("pc" "per cases" nil 0)
    ("coh" "coherence" nil 0)
    ("fs" "FinSequence" nil 0)
    ("hb" "hereby" nil 0)
    ("sct" "such that" nil 0)
    ("tco" "the carrier of" nil 0)
    ("reg" "regular" nil 0)
    ("ts" "thesis" nil 0)
    ("rec" "reconsider" nil 0)
    ("eq"  "equals" nil 0)
    ("tm"  "theorem" nil 0)
    ("el" "Element" nil 0)
    ("supp" "suppose" nil 0)
    ("rv"   "reserve" nil 0)
    ("corr" "correctness" nil 0)
    ("coh" "coherence" nil 0)
    ("bei" "being" nil 0)
    ("ass" "assume" nil 0)
    ("monot" "monotone" nil 0)
    ("uniq" "uniqueness" nil 0)
    ("df"  "definition" nil 0)
    ("cl" "cluster" nil 0)
    ("exi" "existence" nil 0)
    ("redef" "redefine" nil 0)
    ("carr" "carrier" nil 0)
    ("imp"  "implies" nil 0)
    ("e" "end;" nil 0)
    ))

[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.