More advanced IE script

1 files changed, 74 insertions, 0 deletions

diff --git a/.zsh/functions/IE b/.zsh/functions/IE
new file mode 100644
index 0000000..1c40f45
--- /dev/null
+++ b/.zsh/functions/IE
@@ -0,0 +1,74 @@
+# default arguments to isabelle emacs
+local defargs="-x true -m iff"
+local file logic
+
+# 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 line p=.isabelle-logic
+    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 not logic could be determined
+if [[ -z $logic ]]; then
+    logic="HOL"
+    echo "Defaulting to '$logic'."
+fi
+
+# AAAAND ... FIRE!
+isabelle emacs ${=defargs} -l $logic $file "$@"
+
+# vim: ft=zsh