Admin/check_ml_headers
author wenzelm
Fri, 13 Mar 2009 19:58:26 +0100
changeset 30510 4120fc59dd85
parent 28504 7ad7d7d6df47
child 36859 51af1657263b
permissions -rwxr-xr-x
unified type Proof.method and pervasive METHOD combinators;
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
# $Id$
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
# 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
     6
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     7
# requires some GNU tools
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     8
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     9
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    10
ONLY_FILENAMES=1
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    11
if [ "$1" == "-o" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    12
then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    13
  ONLY_FILENAMES=""
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    14
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    15
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    16
REPORT_EMPTY=""
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    17
if [ "$2" == "-e" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    18
then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    19
  REPORT_EMPTY=1
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    20
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    21
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24618
diff changeset
    22
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    23
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    24
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    25
do
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    26
  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
    27
  FILELOC="${LOC:${#ISABELLE_SRC}}"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    28
  if [ "$TITLE" != "$FILELOC" ]
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 "$REPORT_EMPTY" -o -n "$TITLE" ]
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
      if [ -n "$ONLY_FILENAMES" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    33
      then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    34
        echo "Inconsistency in $LOC: $TITLE"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    35
      else
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    36
        echo "$LOC"
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
    fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    39
  fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    40
done