haftmann@24618: #!/usr/bin/env bash
haftmann@24618: #
haftmann@37741: # check_ml_headers - check headers of *.ML files in distribution for inconsistencies
haftmann@24618: #
haftmann@24618: # requires some GNU tools
haftmann@24618: #
haftmann@24618: 
haftmann@37741: ONLY_FILENAMES=""
haftmann@24618: if [ "$1" == "-o" ]
haftmann@24618: then
haftmann@37741:   ONLY_FILENAMES=1
haftmann@24618: fi
haftmann@24618: 
haftmann@24618: REPORT_EMPTY=""
haftmann@24618: if [ "$2" == "-e" ]
haftmann@24618: then
haftmann@24618:   REPORT_EMPTY=1
haftmann@24618: fi
haftmann@24618: 
wenzelm@28504: ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
haftmann@24618: 
haftmann@24618: for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
haftmann@24618: do
haftmann@24618:   TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
haftmann@24618:   FILELOC="${LOC:${#ISABELLE_SRC}}"
haftmann@24618:   if [ "$TITLE" != "$FILELOC" ]
haftmann@24618:   then
haftmann@37741:     if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ]
haftmann@24618:     then
haftmann@37741:       if [ -z "$ONLY_FILENAMES" ]
haftmann@24618:       then
haftmann@24618:         echo "Inconsistency in $LOC: $TITLE"
haftmann@24618:       else
haftmann@24618:         echo "$LOC"
haftmann@24618:       fi
haftmann@24618:     fi
haftmann@24618:   fi
haftmann@24618: done