Commit 62a213aa authored by MARCHE Claude's avatar MARCHE Claude
Browse files

new dir for isabelle2014

parent 37fa5ab1
chapter Why3
session Why3 = HOL +
options [document = false]
theories Why3
#!/usr/bin/env bash
#
# DESCRIPTION: process files generated by Why3
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] WHY3_FILE"
echo
echo " Options are:"
echo " -b batch mode"
echo " -i NAME interactive mode using interface NAME"
echo
echo "Process files generated by Why3."
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## utilities
function make_theory()
{
BNAME=`basename "$1"`
if [ ! -e "$1.thy" ]; then
echo -e "theory $BNAME\nimports Why3\nbegin\n\nwhy3_open \"$BNAME.xml\"\n" > "$1.thy"
sed \
-e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
-e 's/<[^l][^>]*>//g' \
"$1.xml" >> "$1.thy"
echo -e "why3_end\n\nend" >> "$1.thy"
fi
}
## process command line
while getopts "bi:" OPT
do
case "$OPT" in
b)
BATCH=true
;;
i)
INTERACTIVE=true
INTERFACE="$OPTARG"
;;
\?)
usage
;;
esac
done
## main
shift $(($OPTIND - 1))
[ "$#" != 1 ] && usage
NAME=`dirname "$1"`/`basename "$1" .xml`
if [ "$BATCH" = true ]; then
"$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
elif [ "$INTERACTIVE" = true ]; then
make_theory "$NAME"
case "$INTERFACE" in
emacs)
"$ISABELLE_TOOL" emacs -L Why3 "${NAME}.thy"
;;
jedit)
if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
"$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
-reuseview -wait "$(jvmpath "${NAME}.thy")"
else
"$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
fi
;;
*)
fail "Unknown Isabelle interface: \"$INTERFACE\""
;;
esac
else
usage
fi
#!/usr/bin/env bash
#
# DESCRIPTION: Isabelle/jEdit with Why3 session and server port
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [ARGS...]"
echo
echo "Start Isabelle/jEdit with Why3 session and server port, for quick invocation"
echo "via why3ide."
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## main
[ "$1" = "-?" ] && usage
SERVER_FILE="$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER"
if [ -f "$SERVER_FILE" ]; then
fail "Server already running: \"$SERVER_FILE\""
else
exec "$ISABELLE_TOOL" jedit "-j-server=$WHY3_JEDIT_SERVER" -l Why3 "$@"
fi
# -*- shell-script -*- :mode=shellscript:
WHY3_ISABELLE_HOME="$COMPONENT"
WHY3_JEDIT_SERVER="server-Why3"
ISABELLE_TOOLS="$ISABELLE_TOOLS:$WHY3_ISABELLE_HOME/Tools"
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment