Admin/check_ml_headers
author wenzelm
Sat Oct 04 17:40:56 2008 +0200 (2008-10-04)
changeset 28504 7ad7d7d6df47
parent 24618 6ab574864cd4
child 36859 51af1657263b
permissions -rwxr-xr-x
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
haftmann@24618
     1
#!/usr/bin/env bash
haftmann@24618
     2
#
haftmann@24618
     3
# $Id$
haftmann@24618
     4
#
haftmann@24618
     5
# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
haftmann@24618
     6
#
haftmann@24618
     7
# requires some GNU tools
haftmann@24618
     8
#
haftmann@24618
     9
haftmann@24618
    10
ONLY_FILENAMES=1
haftmann@24618
    11
if [ "$1" == "-o" ]
haftmann@24618
    12
then
haftmann@24618
    13
  ONLY_FILENAMES=""
haftmann@24618
    14
fi
haftmann@24618
    15
haftmann@24618
    16
REPORT_EMPTY=""
haftmann@24618
    17
if [ "$2" == "-e" ]
haftmann@24618
    18
then
haftmann@24618
    19
  REPORT_EMPTY=1
haftmann@24618
    20
fi
haftmann@24618
    21
wenzelm@28504
    22
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
haftmann@24618
    23
haftmann@24618
    24
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
haftmann@24618
    25
do
haftmann@24618
    26
  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
haftmann@24618
    27
  FILELOC="${LOC:${#ISABELLE_SRC}}"
haftmann@24618
    28
  if [ "$TITLE" != "$FILELOC" ]
haftmann@24618
    29
  then
haftmann@24618
    30
    if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
haftmann@24618
    31
    then
haftmann@24618
    32
      if [ -n "$ONLY_FILENAMES" ]
haftmann@24618
    33
      then
haftmann@24618
    34
        echo "Inconsistency in $LOC: $TITLE"
haftmann@24618
    35
      else
haftmann@24618
    36
        echo "$LOC"
haftmann@24618
    37
      fi
haftmann@24618
    38
    fi
haftmann@24618
    39
  fi
haftmann@24618
    40
done