blob: c65c93b38eeb4af2363a7fdb7b60a13061a5eac3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
readonly default="HOL"
local file logic program defargs
if [[ $0 == "IJ" ]]; then
program="jedit"
defargs=""
else
program="emacs"
defargs="-x true -m iff"
fi
# safety check to avoid failing later on
if [[ ! -x =isabelle ]]; then
echo "Isabelle not found. Aborting"
return 1
fi
# try to map the arguments to the correct option
# usage is: [logic] [file] [isabelle opts]
case x$1 in
x*.thy) file=$1; shift;;
x-*);; # argument to isabelle emacs -> ignore
x) ;; # empty -> ignore
x*) # a logic pattern :)
logic=$1; shift
if [[ -n $1 && $1 != -* ]]; then
file=$1; shift
fi
esac
# have a .isabelle-logic file that contains a logic-image pattern
# if it contains "..", the parent directory is searched
if [[ -z $logic && -e .isabelle-logic ]]; then
local p=.isabelle-logic
local line=$(head -1 $p)
while [[ $line == .. ]]; do
p=../$p
if [[ -e $p ]]; then
line=$(head -1 $p)
else
line=
fi
done
if [[ -n $line ]]; then
logic=$line
echo "Setting logic to '$logic' as found in local settings."
fi
fi
# try to find the correct logic
# special case HOL, just to be sure :)
if [[ -n $logic && $logic != "HOL" ]]; then
local found
for l in $(isabelle findlogics); do
if [[ $l == *${logic}* ]]; then
logic=$l; found=1
echo "Using logic '$logic'"
break
fi
done
if [[ -z $found ]]; then
echo "No logic found that matches the pattern *${logic}*"
echo "Existing logics are: $(isabelle findlogics)"
unset logic
fi
fi
# fall-through if no logic could be determined
if [[ -z $logic ]]; then
logic=$default
echo "Defaulting to '$logic'."
fi
# AAAAND ... FIRE!
isabelle ${program} ${=defargs} "$@" -l $logic $file
# vim: ft=zsh
|
