diff options
Diffstat (limited to '')
| -rw-r--r-- | .zsh/functions/IE | 17 |
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 &! |