|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Makarius |
|
4 # |
|
5 # DESCRIPTION: run Isabelle process with raw ML console and line editor |
|
6 |
|
7 PRG="$(basename "$0")" |
|
8 |
|
9 function usage() |
|
10 { |
|
11 echo |
|
12 echo "Usage: isabelle $PRG [OPTIONS]" |
|
13 echo |
|
14 echo " Options are:" |
|
15 echo " -d DIR include session directory" |
|
16 echo " -l NAME logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")" |
|
17 echo " -m MODE add print mode for output" |
|
18 echo " -n no build of session image on startup" |
|
19 echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" |
|
20 echo " -s system build mode for session image" |
|
21 echo |
|
22 echo " Run Isabelle process with raw ML console and line editor" |
|
23 echo " (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")." |
|
24 echo |
|
25 exit 1 |
|
26 } |
|
27 |
|
28 |
|
29 ## process command line |
|
30 |
|
31 # options |
|
32 |
|
33 declare -a ISABELLE_OPTIONS=() |
|
34 declare -a BUILD_OPTIONS=() |
|
35 |
|
36 LOGIC="$ISABELLE_LOGIC" |
|
37 DO_BUILD="true" |
|
38 |
|
39 while getopts "d:l:m:no:s" OPT |
|
40 do |
|
41 case "$OPT" in |
|
42 d) |
|
43 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-d" |
|
44 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" |
|
45 ;; |
|
46 l) |
|
47 LOGIC="$OPTARG" |
|
48 ;; |
|
49 m) |
|
50 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m" |
|
51 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG" |
|
52 ;; |
|
53 n) |
|
54 DO_BUILD="false" |
|
55 ;; |
|
56 o) |
|
57 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o" |
|
58 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG" |
|
59 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-o" |
|
60 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" |
|
61 ;; |
|
62 s) |
|
63 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-s" |
|
64 ;; |
|
65 \?) |
|
66 usage |
|
67 ;; |
|
68 esac |
|
69 done |
|
70 |
|
71 shift $(($OPTIND - 1)) |
|
72 |
|
73 |
|
74 # args |
|
75 |
|
76 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
|
77 |
|
78 |
|
79 ## main |
|
80 |
|
81 if [ "$DO_BUILD" = true ] |
|
82 then |
|
83 "$ISABELLE_TOOL" build -b -n "${BUILD_OPTIONS[@]}" "$LOGIC" >/dev/null 2>/dev/null || |
|
84 { |
|
85 echo "Build started for Isabelle/$LOGIC" |
|
86 "$ISABELLE_TOOL" build -b "${BUILD_OPTIONS[@]}" "$LOGIC" || exit "$?" |
|
87 } |
|
88 fi |
|
89 |
|
90 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
|
91 then |
|
92 exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC" |
|
93 else |
|
94 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
|
95 exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC" |
|
96 fi |