53 shift $(($OPTIND - 1)) |
53 shift $(($OPTIND - 1)) |
54 |
54 |
55 |
55 |
56 # args |
56 # args |
57 |
57 |
58 NAME="-" |
58 TEXT="" |
59 [ "$#" -ge 1 ] && { NAME="$1"; shift; } |
59 [ "$#" -ge 1 ] && { TEXT="$1"; shift; } |
60 |
60 |
61 [ "$#" -ne 0 -o "$NAME" = "-" ] && usage |
61 [ "$#" -ne 0 ] && usage |
62 |
62 |
63 |
63 |
64 ## main |
64 ## main |
65 |
65 |
66 if [ -z "$OUTPUT" ]; then |
66 case "$OUTPUT_NAME" in |
67 OUTPUT=$(echo "$NAME" | tr A-Z a-z) |
67 "") |
68 [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}" |
68 OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z) |
69 OUTPUT="isabelle${OUTPUT}.pdf" |
69 if [ -z "$OUTPUT_NAME" ]; then |
70 OUTPUT_FORMAT="pdf" |
70 OUTPUT_NAME="isabelle" |
71 else |
71 else |
72 case "$OUTPUT" in |
72 OUTPUT_NAME="isabelle_${OUTPUT_NAME}" |
73 *.eps) |
73 fi |
74 OUTPUT_FORMAT="eps" |
74 ;; |
75 ;; |
75 */* | *.eps | *.pdf) |
76 *.pdf) |
76 fail "Bad output base name: \"$OUTPUT_NAME\"" |
77 OUTPUT_FORMAT="pdf" |
77 ;; |
78 ;; |
78 *) |
79 *) |
79 ;; |
80 fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\"" |
80 esac |
81 ;; |
|
82 esac |
|
83 fi |
|
84 |
81 |
85 [ -z "$QUIET" ] && echo "$OUTPUT" >&2 |
82 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2 |
|
83 perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps" |
86 |
84 |
87 if [ "$OUTPUT_FORMAT" = "eps" ]; then |
85 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2 |
88 perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT" |
86 "$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps" |
89 else |
87 |
90 perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \ |
|
91 "$ISABELLE_EPSTOPDF" -f > "$OUTPUT" |
|
92 fi |
|