| author | wenzelm | 
| Tue, 20 Apr 2010 17:07:53 +0200 | |
| changeset 36238 | 344377ce2e0a | 
| parent 35022 | c844b93dd147 | 
| child 52439 | 4cf3f6153eb8 | 
| permissions | -rwxr-xr-x | 
| 24875 | 1  | 
#!/usr/bin/env bash  | 
2  | 
#  | 
|
3  | 
# Author: Makarius  | 
|
4  | 
#  | 
|
5  | 
# DESCRIPTION: generate outer syntax keyword files from session logs  | 
|
6  | 
||
7  | 
||
8  | 
## diagnostics  | 
|
9  | 
||
10  | 
PRG="$(basename "$0")"  | 
|
11  | 
||
12  | 
function usage()  | 
|
13  | 
{
 | 
|
14  | 
echo  | 
|
| 28650 | 15  | 
echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"  | 
| 24875 | 16  | 
echo  | 
17  | 
echo " Options are:"  | 
|
18  | 
echo " -k NAME specific name of keywords collection (default: empty)"  | 
|
19  | 
echo  | 
|
20  | 
echo " Generate outer syntax keyword files from (compressed) session LOGS."  | 
|
| 33684 | 21  | 
echo " Targets Emacs Proof General."  | 
| 24875 | 22  | 
echo  | 
23  | 
exit 1  | 
|
24  | 
}  | 
|
25  | 
||
26  | 
||
27  | 
## process command line  | 
|
28  | 
||
29  | 
# options  | 
|
30  | 
||
31  | 
KEYWORDS_NAME=""  | 
|
32  | 
||
| 33684 | 33  | 
while getopts "k:" OPT  | 
| 24875 | 34  | 
do  | 
35  | 
case "$OPT" in  | 
|
36  | 
k)  | 
|
37  | 
KEYWORDS_NAME="$OPTARG"  | 
|
38  | 
;;  | 
|
39  | 
\?)  | 
|
40  | 
usage  | 
|
41  | 
;;  | 
|
42  | 
esac  | 
|
43  | 
done  | 
|
44  | 
||
45  | 
shift $(($OPTIND - 1))  | 
|
46  | 
||
47  | 
||
48  | 
## main  | 
|
49  | 
||
50  | 
SESSIONS=""  | 
|
| 33684 | 51  | 
for LOG in "$@"  | 
| 24875 | 52  | 
do  | 
53  | 
NAME="$(basename "$LOG" .gz)"  | 
|
| 24885 | 54  | 
if [ -z "$SESSIONS" ]; then  | 
55  | 
SESSIONS="$NAME"  | 
|
56  | 
else  | 
|
57  | 
SESSIONS="$SESSIONS + $NAME"  | 
|
| 24875 | 58  | 
fi  | 
59  | 
done  | 
|
60  | 
||
| 33684 | 61  | 
for LOG in "$@"  | 
| 24875 | 62  | 
do  | 
63  | 
  if [ "${LOG%.gz}" = "$LOG" ]; then
 | 
|
64  | 
cat "$LOG"  | 
|
65  | 
else  | 
|
66  | 
gzip -dc "$LOG"  | 
|
67  | 
fi  | 
|
68  | 
echo  | 
|
| 
35022
 
c844b93dd147
modernized perl scripts: prefer standalone executables;
 
wenzelm 
parents: 
33684 
diff
changeset
 | 
69  | 
done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS"  |