summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRené 'Necoro' Neumann <necoro@necoro.eu>2018-06-10 17:36:54 +0200
committerRené 'Necoro' Neumann <necoro@necoro.eu>2018-06-10 17:36:55 +0200
commitba18a34dff9d2b6cc59a82643b61705b4f9937df (patch)
tree1bcfc22f6aa9631def1e822726f3077dfcc743c8
parentba497ab995a125c794398e1c211cd5dbd43f062d (diff)
downloaddotfiles-ba18a34dff9d2b6cc59a82643b61705b4f9937df.tar.gz
dotfiles-ba18a34dff9d2b6cc59a82643b61705b4f9937df.tar.bz2
dotfiles-ba18a34dff9d2b6cc59a82643b61705b4f9937df.zip
[zsh] Remove obsolete isabelle functions
-rw-r--r--.zsh/functions/IE111
l---------.zsh/functions/IJ1
2 files changed, 0 insertions, 112 deletions
diff --git a/.zsh/functions/IE b/.zsh/functions/IE
deleted file mode 100644
index d067f13..0000000
--- a/.zsh/functions/IE
+++ /dev/null
@@ -1,111 +0,0 @@
-# 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
diff --git a/.zsh/functions/IJ b/.zsh/functions/IJ
deleted file mode 120000
index ae92333..0000000
--- a/.zsh/functions/IJ
+++ /dev/null
@@ -1 +0,0 @@
-IE \ No newline at end of file