summaryrefslogtreecommitdiff
path: root/.zsh/functions/IE
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--.zsh/functions/IE17
1 files changed, 15 insertions, 2 deletions
diff --git a/.zsh/functions/IE b/.zsh/functions/IE
index 989cdec..d067f13 100644
--- a/.zsh/functions/IE
+++ b/.zsh/functions/IE
@@ -15,14 +15,16 @@
# or '..', which makes the script take the .isabelle-logic in the parent directory.
readonly default="HOL"
-local file logic program defargs
+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
@@ -63,12 +65,19 @@ if [[ -z $logic && -e .isabelle-logic ]]; then
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 [[ -n $logic && $logic != "HOL" ]]; then
+# 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
@@ -92,6 +101,10 @@ if [[ -z $logic ]]; then
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 &!