blob: d067f13b8ce3970ef0ede9fc4bee4f1c3552d8d3 (
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
# This function is a wrapper around 'isabelle {emacs,jedit}'
# Usage: IE [logic-pattern] [file] [options]
# IJ ...
#
# IE launches emacs, IJ jedit
#
# - logic-pattern: this is expanded to *logic-pattern* and matched
# against all logics as returned by `isabelle findlogics`
# the first match wins
# - file: file to open
# - options: options passed verbatim to 'isabelle emacs'
#
# If no logic-pattern is given, the file .isabelle-logic is
# evaluated: This file should contain one line, being either the logic to load,
# or '..', which makes the script take the .isabelle-logic in the parent directory.
readonly default="HOL"
local file logic program defargs sessiondir usesessions
if [[ $0 == "IJ" ]]; then
program="jedit"
defargs=""
usesessions=1
else
program="emacs"
defargs="-x true -m iff"
usesessions=
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
if [[ -n $2 && $2 != -* ]]; then
file=$2
shift 2
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."
if [[ -n $usesessions ]]; then
sessiondir=$(head -2 $p | tail -1)
[[ $sessiondir == $logic ]] && sessiondir=
[[ -n $sessiondir ]] && echo "Setting sessiondir to '$sessiondir' as found in local settings."
fi
fi
fi
# try to find the correct logic
# special case HOL, just to be sure :)
# if sessiondir is set, we have to use SESSION logic, which is not checked here
if [[ -n $logic && $logic != "HOL" && -z $sessiondir && -z $usesessions ]]; 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
if [[ -n $usesessions && -n $sessiondir ]]; then
defargs="$defargs -d $sessiondir"
fi
# AAAAND ... FIRE! (in the background)
isabelle ${program} ${=defargs} "$@" -l $logic $file &!
# vim: ft=zsh
|
