Admin/check_ml_headers
author wenzelm
Thu Nov 26 15:28:42 2009 +0100 (2009-11-26)
changeset 33905 5760ba045bf0
parent 28504 7ad7d7d6df47
child 36859 51af1657263b
permissions -rwxr-xr-x
additional menu entries;
haftmann@24618
     1
#!/usr/bin/env bash
haftmann@24618
     2
#
haftmann@24618
     3
# $Id$
haftmann@24618
     4
#
haftmann@24618
     5
# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
haftmann@24618
     6
#
haftmann@24618
     7
# requires some GNU tools
haftmann@24618
     8
#
haftmann@24618
     9
haftmann@24618
    10
ONLY_FILENAMES=1
haftmann@24618
    11
if [ "$1" == "-o" ]
haftmann@24618
    12
then
haftmann@24618
    13
  ONLY_FILENAMES=""
haftmann@24618
    14
fi
haftmann@24618
    15
haftmann@24618
    16
REPORT_EMPTY=""
haftmann@24618
    17
if [ "$2" == "-e" ]
haftmann@24618
    18
then
haftmann@24618
    19
  REPORT_EMPTY=1
haftmann@24618
    20
fi
haftmann@24618
    21
wenzelm@28504
    22
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
haftmann@24618
    23
haftmann@24618
    24
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
haftmann@24618
    25
do
haftmann@24618
    26
  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
haftmann@24618
    27
  FILELOC="${LOC:${#ISABELLE_SRC}}"
haftmann@24618
    28
  if [ "$TITLE" != "$FILELOC" ]
haftmann@24618
    29
  then
haftmann@24618
    30
    if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
haftmann@24618
    31
    then
haftmann@24618
    32
      if [ -n "$ONLY_FILENAMES" ]
haftmann@24618
    33
      then
haftmann@24618
    34
        echo "Inconsistency in $LOC: $TITLE"
haftmann@24618
    35
      else
haftmann@24618
    36
        echo "$LOC"
haftmann@24618
    37
      fi
haftmann@24618
    38
    fi
haftmann@24618
    39
  fi
haftmann@24618
    40
done