#!/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