readonly default="HOL"
local file logic program defargs

if [[ $0 == "IJ" ]]; then
    program="jedit"
    defargs=""
else
    program="emacs"
    defargs="-x true -m iff"
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; 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 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."
    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 no logic could be determined
if [[ -z $logic ]]; then
    logic=$default
    echo "Defaulting to '$logic'."
fi

# AAAAND ... FIRE!
isabelle ${program} ${=defargs} "$@" -l $logic $file

# vim: ft=zsh