From 6ecdf2db6a34500671e396591ab5cba7402bd123 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ren=C3=A9=20=27Necoro=27=20Neumann?= <necoro@necoro.net>
Date: Thu, 21 Nov 2013 13:43:51 +0100
Subject: IE/IJ: Session logic

---
 .zsh/functions/IE | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to '.zsh')

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 &!
 
-- 
cgit v1.2.3