author | wenzelm |
Wed, 02 May 2012 22:40:28 +0200 | |
changeset 48735 | 271980472765 |
parent 37740 | 763feb2abb0d |
permissions | -rwxr-xr-x |
haftmann@24618 | 1 |
#!/usr/bin/env bash |
haftmann@24618 | 2 |
# |
haftmann@37740 | 3 |
# check_ml_headers - check headers of *.ML files in distribution for inconsistencies |
haftmann@24618 | 4 |
# |
haftmann@24618 | 5 |
# requires some GNU tools |
haftmann@24618 | 6 |
# |
haftmann@24618 | 7 |
|
haftmann@37740 | 8 |
ONLY_FILENAMES="" |
haftmann@24618 | 9 |
if [ "$1" == "-o" ] |
haftmann@24618 | 10 |
then |
haftmann@37740 | 11 |
ONLY_FILENAMES=1 |
haftmann@24618 | 12 |
fi |
haftmann@24618 | 13 |
|
haftmann@24618 | 14 |
REPORT_EMPTY="" |
haftmann@24618 | 15 |
if [ "$2" == "-e" ] |
haftmann@24618 | 16 |
then |
haftmann@24618 | 17 |
REPORT_EMPTY=1 |
haftmann@24618 | 18 |
fi |
haftmann@24618 | 19 |
|
wenzelm@28504 | 20 |
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/" |
haftmann@24618 | 21 |
|
haftmann@24618 | 22 |
for LOC in $(find "$ISABELLE_SRC" -name "*.ML") |
haftmann@24618 | 23 |
do |
haftmann@24618 | 24 |
TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" |
haftmann@24618 | 25 |
FILELOC="${LOC:${#ISABELLE_SRC}}" |
haftmann@24618 | 26 |
if [ "$TITLE" != "$FILELOC" ] |
haftmann@24618 | 27 |
then |
haftmann@37740 | 28 |
if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] |
haftmann@24618 | 29 |
then |
haftmann@37740 | 30 |
if [ -z "$ONLY_FILENAMES" ] |
haftmann@24618 | 31 |
then |
haftmann@24618 | 32 |
echo "Inconsistency in $LOC: $TITLE" |
haftmann@24618 | 33 |
else |
haftmann@24618 | 34 |
echo "$LOC" |
haftmann@24618 | 35 |
fi |
haftmann@24618 | 36 |
fi |
haftmann@24618 | 37 |
fi |
haftmann@24618 | 38 |
done |