Admin/check_ml_headers
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 06 Sep 2010 16:56:22 +0200
branchisac-update-Isa09-2
changeset 37983 03bfbc480107
parent 36866 51af1657263b
child 37740 763feb2abb0d
permissions -rwxr-xr-x
corrected format for axioms in remaining theories
     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=1
     9 if [ "$1" == "-o" ]
    10 then
    11   ONLY_FILENAMES=""
    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 "$REPORT_EMPTY" -o -n "$TITLE" ]
    29     then
    30       if [ -n "$ONLY_FILENAMES" ]
    31       then
    32         echo "Inconsistency in $LOC: $TITLE"
    33       else
    34         echo "$LOC"
    35       fi
    36     fi
    37   fi
    38 done