Admin/check_ml_headers
author haftmann
Mon, 05 Jul 2010 15:12:20 +0200
changeset 37715 44b27ea94a16
parent 36859 51af1657263b
child 37741 763feb2abb0d
permissions -rwxr-xr-x
tuned proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     2
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     3
# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     4
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     5
# requires some GNU tools
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     6
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     7
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     8
ONLY_FILENAMES=1
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     9
if [ "$1" == "-o" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    10
then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    11
  ONLY_FILENAMES=""
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    12
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    13
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    14
REPORT_EMPTY=""
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    15
if [ "$2" == "-e" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    16
then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    17
  REPORT_EMPTY=1
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    18
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    19
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24618
diff changeset
    20
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    21
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    22
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    23
do
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    24
  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    25
  FILELOC="${LOC:${#ISABELLE_SRC}}"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    26
  if [ "$TITLE" != "$FILELOC" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    27
  then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    28
    if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    29
    then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    30
      if [ -n "$ONLY_FILENAMES" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    31
      then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    32
        echo "Inconsistency in $LOC: $TITLE"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    33
      else
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    34
        echo "$LOC"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    35
      fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    36
    fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    37
  fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    38
done