Admin/maketags
author huffman
Tue Jul 12 18:26:44 2005 +0200 (2005-07-12)
changeset 16777 555c8951f05c
parent 12721 226fc0e2e7e3
permissions -rwxr-xr-x
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 
     5 find . \( -name \*.ML -o -name \*.sml -o -name \*.sig \) -print | \
     6   etags \
     7     --language=none \
     8     --regex='/[ \t]*structure +\([A-Za-z_0-9]+\)/\1/' \
     9     --regex='/[ \t]*functor +\([A-Za-z_0-9]+\)/\1/' \
    10     --regex='/[ \t]*signature +\([A-Za-z_0-9]+\)/\1/' \
    11     --regex='/[ \t]*fun +\([A-Za-z_0-9]+\)/\1/' \
    12     --regex='/[ \t]*val +\([A-Za-z_0-9]+\)/\1/' \
    13     --regex='/[ \t]*and +\([A-Za-z_0-9]+\)/\1/' \
    14     --regex='/[ \t]*exception +\([A-Za-z_0-9]+\)/\1/' \
    15     --regex='/[ \t]*type +\([A-Za-z_0-9]+\)/\1/' \
    16     --regex='/[ \t]*datatype +\([A-Za-z_0-9]+\)/\1/' \
    17     --regex='/[ \t]*= +\([A-Z_]+\)/\1/' \
    18     --regex='/[ \t]*| +\([A-Z_]+\)/\1/' \
    19     -
    20 
    21 find . -type f -print | \
    22   fgrep -v .ML | \
    23   fgrep -v .sml | \
    24   fgrep -v .sig | \
    25   fgrep -v TAGS | \
    26   etags --language=none --append -