added script checking for consistency of ML file header
authorhaftmann
Tue Sep 18 07:36:09 2007 +0200 (2007-09-18)
changeset 246186ab574864cd4
parent 24617 bc484b2671fd
child 24619 c2e6a0f8c30b
added script checking for consistency of ML file header
Admin/check_ml_headers
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/check_ml_headers	Tue Sep 18 07:36:09 2007 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     1.9 +#
    1.10 +# requires some GNU tools
    1.11 +#
    1.12 +
    1.13 +ONLY_FILENAMES=1
    1.14 +if [ "$1" == "-o" ]
    1.15 +then
    1.16 +  ONLY_FILENAMES=""
    1.17 +fi
    1.18 +
    1.19 +REPORT_EMPTY=""
    1.20 +if [ "$2" == "-e" ]
    1.21 +then
    1.22 +  REPORT_EMPTY=1
    1.23 +fi
    1.24 +
    1.25 +ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/"
    1.26 +
    1.27 +for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
    1.28 +do
    1.29 +  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
    1.30 +  FILELOC="${LOC:${#ISABELLE_SRC}}"
    1.31 +  if [ "$TITLE" != "$FILELOC" ]
    1.32 +  then
    1.33 +    if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
    1.34 +    then
    1.35 +      if [ -n "$ONLY_FILENAMES" ]
    1.36 +      then
    1.37 +        echo "Inconsistency in $LOC: $TITLE"
    1.38 +      else
    1.39 +        echo "$LOC"
    1.40 +      fi
    1.41 +    fi
    1.42 +  fi
    1.43 +done