equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash -x |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # DESCRIPTION: prepare theory session document |
5 # DESCRIPTION: prepare theory session document |
6 |
6 |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
|
16 echo " -c clean -- remove DIR after succesful run" |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
17 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps," |
17 echo " ps.gz, pdf" |
18 echo " ps.gz, pdf" |
18 echo |
19 echo |
19 echo " Prepare the theory session document in DIR (default '.')" |
20 echo " Prepare the theory session document in DIR (default 'document')" |
20 echo " producing the specified output format." |
21 echo " producing the specified output format." |
21 echo |
22 echo |
22 exit 1 |
23 exit 1 |
23 } |
24 } |
24 |
25 |
31 |
32 |
32 ## process command line |
33 ## process command line |
33 |
34 |
34 # options |
35 # options |
35 |
36 |
|
37 CLEAN="" |
36 OUTFORMAT=dvi |
38 OUTFORMAT=dvi |
37 |
39 |
38 while getopts "o:" OPT |
40 while getopts "co:" OPT |
39 do |
41 do |
40 case "$OPT" in |
42 case "$OPT" in |
|
43 c) |
|
44 CLEAN=true |
|
45 ;; |
41 o) |
46 o) |
42 OUTFORMAT="$OPTARG" |
47 OUTFORMAT="$OPTARG" |
43 ;; |
48 ;; |
44 \?) |
49 \?) |
45 usage |
50 usage |
50 shift $(($OPTIND - 1)) |
55 shift $(($OPTIND - 1)) |
51 |
56 |
52 |
57 |
53 # args |
58 # args |
54 |
59 |
55 DIR="." |
60 DIR="document" |
56 [ $# -ge 1 ] && { DIR="$1"; shift; } |
61 [ $# -ge 1 ] && { DIR="$1"; shift; } |
57 |
62 |
58 [ $# -ne 0 ] && usage |
63 [ $# -ne 0 ] && usage |
59 |
64 |
60 |
65 |
71 esac |
76 esac |
72 |
77 |
73 |
78 |
74 # prepare document |
79 # prepare document |
75 |
80 |
76 cd "$DIR" || fail "Bad directory '$DIR'" |
|
77 |
|
78 function pre_latex () |
81 function pre_latex () |
79 { |
82 { |
80 local FMT="$1" |
83 local FMT="$1" |
81 rm -f *.aux |
84 rm -f *.aux |
82 if [ -f root.bib ] |
85 if [ -f root.bib ] |
87 else |
90 else |
88 $ISATOOL latex -o "$FMT" |
91 $ISATOOL latex -o "$FMT" |
89 fi |
92 fi |
90 } |
93 } |
91 |
94 |
92 if [ -f IsaMakefile ]; then |
95 ( |
93 $ISATOOL make "$OUTFORMAT" |
96 cd "$DIR" || fail "Bad directory '$DIR'" |
94 RC=$? #FIXME !?? |
97 |
95 elif [ "$OUTFORMAT" = pdf ]; then |
98 if [ -f IsaMakefile ]; then |
96 pre_latex pdf && \ |
99 $ISATOOL make "$OUTFORMAT" |
97 $ISATOOL latex -o pdf && \ |
100 RC=$? |
98 { if [ -n "$ISABELLE_THUMBPDF" ]; then |
101 elif [ "$OUTFORMAT" = pdf ]; then |
99 $ISATOOL latex -o png && \ |
102 pre_latex pdf && \ |
100 $ISATOOL latex -o pdf |
103 $ISATOOL latex -o pdf && \ |
101 fi; } |
104 { if [ -n "$ISABELLE_THUMBPDF" ]; then |
102 RC=$? |
105 $ISATOOL latex -o png && \ |
103 else |
106 $ISATOOL latex -o pdf |
104 pre_latex dvi && \ |
107 fi; } |
105 $ISATOOL latex -o "$OUTFORMAT" |
108 RC=$? |
106 RC=$? |
109 else |
107 fi |
110 pre_latex dvi && \ |
|
111 $ISATOOL latex -o "$OUTFORMAT" |
|
112 RC=$? |
|
113 fi |
|
114 |
|
115 [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \ |
|
116 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" |
|
117 |
|
118 exit $RC |
|
119 ) |
|
120 RC=$? |
108 |
121 |
109 |
122 |
110 # install |
123 # install |
111 |
124 |
112 [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'" |
125 [ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'" |
113 cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" |
126 |
|
127 #beware! |
|
128 [ -n "$CLEAN" ] && rm -rf "$DIR" |
|
129 |
|
130 exit "$RC" |