Admin/check_ml_headers
author haftmann
Tue Sep 18 07:36:09 2007 +0200 (2007-09-18)
changeset 24618 6ab574864cd4
child 28504 7ad7d7d6df47
permissions -rwxr-xr-x
added script checking for consistency of ML file header
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     6 #
     7 # requires some GNU tools
     8 #
     9 
    10 ONLY_FILENAMES=1
    11 if [ "$1" == "-o" ]
    12 then
    13   ONLY_FILENAMES=""
    14 fi
    15 
    16 REPORT_EMPTY=""
    17 if [ "$2" == "-e" ]
    18 then
    19   REPORT_EMPTY=1
    20 fi
    21 
    22 ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/"
    23 
    24 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
    25 do
    26   TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
    27   FILELOC="${LOC:${#ISABELLE_SRC}}"
    28   if [ "$TITLE" != "$FILELOC" ]
    29   then
    30     if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
    31     then
    32       if [ -n "$ONLY_FILENAMES" ]
    33       then
    34         echo "Inconsistency in $LOC: $TITLE"
    35       else
    36         echo "$LOC"
    37       fi
    38     fi
    39   fi
    40 done