author | hoelzl |
Thu, 09 Jun 2016 16:11:33 +0200 | |
changeset 63262 | e497387de7af |
parent 37741 | 763feb2abb0d |
permissions | -rwxr-xr-x |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
2 |
# |
37741 | 3 |
# check_ml_headers - check headers of *.ML files in distribution for inconsistencies |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
4 |
# |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
5 |
# requires some GNU tools |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
6 |
# |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
7 |
|
37741 | 8 |
ONLY_FILENAMES="" |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
9 |
if [ "$1" == "-o" ] |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
10 |
then |
37741 | 11 |
ONLY_FILENAMES=1 |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
12 |
fi |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
13 |
|
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
14 |
REPORT_EMPTY="" |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
15 |
if [ "$2" == "-e" ] |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
16 |
then |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
17 |
REPORT_EMPTY=1 |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
18 |
fi |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
19 |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
24618
diff
changeset
|
20 |
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/" |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
21 |
|
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
22 |
for LOC in $(find "$ISABELLE_SRC" -name "*.ML") |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
23 |
do |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
24 |
TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
25 |
FILELOC="${LOC:${#ISABELLE_SRC}}" |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
26 |
if [ "$TITLE" != "$FILELOC" ] |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
27 |
then |
37741 | 28 |
if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
29 |
then |
37741 | 30 |
if [ -z "$ONLY_FILENAMES" ] |
24618
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
31 |
then |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
32 |
echo "Inconsistency in $LOC: $TITLE" |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
33 |
else |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
34 |
echo "$LOC" |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
35 |
fi |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
36 |
fi |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
37 |
fi |
6ab574864cd4
added script checking for consistency of ML file header
haftmann
parents:
diff
changeset
|
38 |
done |