equal
deleted
inserted
replaced
|
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 # |
|
9 |
|
10 ONLY_FILENAMES=1 |
|
11 if [ "$1" == "-o" ] |
|
12 then |
|
13 ONLY_FILENAMES="" |
|
14 fi |
|
15 |
|
16 REPORT_EMPTY="" |
|
17 if [ "$2" == "-e" ] |
|
18 then |
|
19 REPORT_EMPTY=1 |
|
20 fi |
|
21 |
|
22 ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/" |
|
23 |
|
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 |