Admin/check_ml_headers
author huffman
Tue, 09 Oct 2012 17:33:46 +0200
changeset 49759 ecf1d5d87e5e
parent 37741 763feb2abb0d
permissions -rwxr-xr-x
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options

#!/usr/bin/env bash
#
# check_ml_headers - check headers of *.ML files in distribution for inconsistencies
#
# requires some GNU tools
#

ONLY_FILENAMES=""
if [ "$1" == "-o" ]
then
  ONLY_FILENAMES=1
fi

REPORT_EMPTY=""
if [ "$2" == "-e" ]
then
  REPORT_EMPTY=1
fi

ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"

for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
do
  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
  FILELOC="${LOC:${#ISABELLE_SRC}}"
  if [ "$TITLE" != "$FILELOC" ]
  then
    if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ]
    then
      if [ -z "$ONLY_FILENAMES" ]
      then
        echo "Inconsistency in $LOC: $TITLE"
      else
        echo "$LOC"
      fi
    fi
  fi
done