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