| author | haftmann |
| Tue, 18 Sep 2007 07:36:09 +0200 | |
| changeset 24618 | 6ab574864cd4 |
| child 28504 | 7ad7d7d6df47 |
| permissions | -rwxr-xr-x |
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 #
10 ONLY_FILENAMES=1
11 if [ "$1" == "-o" ]
12 then
13 ONLY_FILENAMES=""
14 fi
16 REPORT_EMPTY=""
17 if [ "$2" == "-e" ]
18 then
19 REPORT_EMPTY=1
20 fi
22 ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/"
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