Admin/check_ml_headers
author wenzelm
Sun May 13 20:24:33 2018 +0200 (14 months ago)
changeset 68172 0f14cf9c632f
parent 37741 763feb2abb0d
permissions -rwxr-xr-x
more concise information;
haftmann@24618
     1
#!/usr/bin/env bash
haftmann@24618
     2
#
haftmann@37741
     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@37741
     8
ONLY_FILENAMES=""
haftmann@24618
     9
if [ "$1" == "-o" ]
haftmann@24618
    10
then
haftmann@37741
    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@37741
    28
    if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ]
haftmann@24618
    29
    then
haftmann@37741
    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