# 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