author | Walther Neuper <wneuper@ist.tugraz.at> |
Tue, 07 Feb 2017 08:57:42 +0100 | |
changeset 59316 | 3a60188d9cc3 |
parent 59180 | 85ec71012df8 |
permissions | -rwxr-xr-x |
wneuper@59180 | 1 |
#!/usr/bin/env bash |
wneuper@59180 | 2 |
# |
wneuper@59180 | 3 |
# check_ml_headers - check headers of *.ML files in distribution for inconsistencies |
wneuper@59180 | 4 |
# |
wneuper@59180 | 5 |
# requires some GNU tools |
wneuper@59180 | 6 |
# |
wneuper@59180 | 7 |
|
wneuper@59180 | 8 |
ONLY_FILENAMES="" |
wneuper@59180 | 9 |
if [ "$1" == "-o" ] |
wneuper@59180 | 10 |
then |
wneuper@59180 | 11 |
ONLY_FILENAMES=1 |
wneuper@59180 | 12 |
fi |
wneuper@59180 | 13 |
|
wneuper@59180 | 14 |
REPORT_EMPTY="" |
wneuper@59180 | 15 |
if [ "$2" == "-e" ] |
wneuper@59180 | 16 |
then |
wneuper@59180 | 17 |
REPORT_EMPTY=1 |
wneuper@59180 | 18 |
fi |
wneuper@59180 | 19 |
|
wneuper@59180 | 20 |
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/" |
wneuper@59180 | 21 |
|
wneuper@59180 | 22 |
for LOC in $(find "$ISABELLE_SRC" -name "*.ML") |
wneuper@59180 | 23 |
do |
wneuper@59180 | 24 |
TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" |
wneuper@59180 | 25 |
FILELOC="${LOC:${#ISABELLE_SRC}}" |
wneuper@59180 | 26 |
if [ "$TITLE" != "$FILELOC" ] |
wneuper@59180 | 27 |
then |
wneuper@59180 | 28 |
if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] |
wneuper@59180 | 29 |
then |
wneuper@59180 | 30 |
if [ -z "$ONLY_FILENAMES" ] |
wneuper@59180 | 31 |
then |
wneuper@59180 | 32 |
echo "Inconsistency in $LOC: $TITLE" |
wneuper@59180 | 33 |
else |
wneuper@59180 | 34 |
echo "$LOC" |
wneuper@59180 | 35 |
fi |
wneuper@59180 | 36 |
fi |
wneuper@59180 | 37 |
fi |
wneuper@59180 | 38 |
done |