1#!/usr/bin/env bash 2# 3# check_ml_headers - check headers of *.ML files in distribution for inconsistencies 4# 5# requires some GNU tools 6# 7 8ONLY_FILENAMES="" 9if [ "$1" == "-o" ] 10then 11 ONLY_FILENAMES=1 12fi 13 14REPORT_EMPTY="" 15if [ "$2" == "-e" ] 16then 17 REPORT_EMPTY=1 18fi 19 20ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/" 21 22for LOC in $(find "$ISABELLE_SRC" -name "*.ML") 23do 24 TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" 25 FILELOC="${LOC:${#ISABELLE_SRC}}" 26 if [ "$TITLE" != "$FILELOC" ] 27 then 28 if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] 29 then 30 if [ -z "$ONLY_FILENAMES" ] 31 then 32 echo "Inconsistency in $LOC: $TITLE" 33 else 34 echo "$LOC" 35 fi 36 fi 37 fi 38done 39