Admin/check_ml_headers
author wenzelm
Fri Mar 07 11:46:26 2014 +0100 (2014-03-07)
changeset 55974 c835a9379026
parent 37741 763feb2abb0d
permissions -rwxr-xr-x
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
     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 
     8 ONLY_FILENAMES=""
     9 if [ "$1" == "-o" ]
    10 then
    11   ONLY_FILENAMES=1
    12 fi
    13 
    14 REPORT_EMPTY=""
    15 if [ "$2" == "-e" ]
    16 then
    17   REPORT_EMPTY=1
    18 fi
    19 
    20 ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
    21 
    22 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
    23 do
    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
    38 done