--- a/Admin/lib/Tools/build_doc Thu Mar 10 12:11:50 2016 +0100
+++ b/Admin/lib/Tools/build_doc Thu Mar 10 17:30:04 2016 +0100
@@ -18,4 +18,4 @@
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
+isabelle java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
--- a/Admin/lib/Tools/check_sources Thu Mar 10 12:11:50 2016 +0100
+++ b/Admin/lib/Tools/check_sources Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Check_Sources "$@"
+isabelle java isabelle.Check_Sources "$@"
--- a/lib/Tools/browser Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/browser Thu Mar 10 17:30:04 2016 +0100
@@ -86,9 +86,9 @@
esac
if [ -z "$OUTFILE" ]; then
- "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
+ isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
else
- "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
+ isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
fi
RC="$?"
@@ -102,7 +102,7 @@
rm -f "$PRIVATE_FILE"
elif [ -z "$ADMIN_BUILD" ]; then
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+ exec isabelle java GraphBrowser.GraphBrowser
else
RC=0
fi
--- a/lib/Tools/build Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/build Thu Mar 10 17:30:04 2016 +0100
@@ -169,7 +169,7 @@
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
+isabelle java "${JAVA_ARGS[@]}" isabelle.Build \
"$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
"$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
--- a/lib/Tools/console Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/console Thu Mar 10 17:30:04 2016 +0100
@@ -21,8 +21,8 @@
if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
then
- exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+ exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
else
echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+ exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
fi
--- a/lib/Tools/doc Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/doc Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Doc "$@"
+isabelle java isabelle.Doc "$@"
--- a/lib/Tools/document Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/document Thu Mar 10 17:30:04 2016 +0100
@@ -128,12 +128,12 @@
./build "$OUTFORMAT" "$NAME"
RC="$?"
else
- "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
- { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
+ isabelle latex -o sty "$ROOT_NAME.tex" && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+ { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
+ { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+ isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
RC="$?"
fi
--- a/lib/Tools/options Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/options Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-exec "$ISABELLE_TOOL" java isabelle.Options "$@"
+exec isabelle java isabelle.Options "$@"
--- a/lib/Tools/process Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/process Thu Mar 10 17:30:04 2016 +0100
@@ -19,4 +19,4 @@
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
+isabelle java isabelle.ML_Process "$@"
--- a/lib/Tools/update_cartouches Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_cartouches Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Cartouches "$@"
+isabelle java isabelle.Update_Cartouches "$@"
--- a/lib/Tools/update_header Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_header Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Header "$@"
+isabelle java isabelle.Update_Header "$@"
--- a/lib/Tools/update_then Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_then Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Then "$@"
+isabelle java isabelle.Update_Then "$@"
--- a/lib/Tools/update_theorems Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_theorems Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
isabelle_admin_build jars || exit $?
-"$ISABELLE_TOOL" java isabelle.Update_Theorems "$@"
+isabelle java isabelle.Update_Theorems "$@"
--- a/src/Doc/Classes/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Classes/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Codegen/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Codegen/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -8,7 +8,7 @@
# ad-hoc patching of temporary path from sources
perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
# clean up afterwards
--- a/src/Doc/Eisbach/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Eisbach/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Eisbach
+isabelle logo Eisbach
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Implementation/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Implementation/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Intro/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Intro/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Isar_Ref/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Isar_Ref/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,7 +5,7 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/JEdit/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/JEdit/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo jEdit
+isabelle logo jEdit
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Logics/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics_ZF/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Logics_ZF/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo ZF
+isabelle logo ZF
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Main/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Main/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/Doc/Nitpick/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Nitpick/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Nitpick
+isabelle logo Nitpick
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Prog_Prove/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Prog_Prove/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo HOL
+isabelle logo HOL
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Sledgehammer/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Sledgehammer/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H"
+isabelle logo -n isabelle_sledgehammer "S/H"
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/System/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/System/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo
+isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Tutorial/document/build Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Tutorial/document/build Thu Mar 10 17:30:04 2016 +0100
@@ -5,10 +5,10 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo HOL
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle logo HOL
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
./isa-index root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/Doc/prepare_document Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/prepare_document Thu Mar 10 17:30:04 2016 +0100
@@ -4,13 +4,13 @@
FORMAT="$1"
-"$ISABELLE_TOOL" latex -o sty
+isabelle latex -o sty
cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
[ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
--- a/src/HOL/Mirabelle/ex/Ex.thy Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mirabelle/ex/Ex.thy Thu Mar 10 17:30:04 2016 +0100
@@ -3,7 +3,7 @@
ML {*
val rc = Isabelle_System.bash
- "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle arith Inner_Product.thy";
+ "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy";
if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
else ();
*} -- "some arbitrary small test case"
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 10 17:30:04 2016 +0100
@@ -158,8 +158,8 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $cmd =
- "\"$ENV{'ISABELLE_TOOL'}\" process " .
- "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
+ "isabelle process -o quick_and_dirty -o threads=1" .
+ " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;
if ($output_log) {
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Thu Mar 10 17:30:04 2016 +0100
@@ -133,7 +133,7 @@
# execution
-"$ISABELLE_TOOL" process -o auto_time_limit=10.0 \
+isabelle process -o auto_time_limit=10.0 \
-e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
--- a/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe Thu Mar 10 17:30:04 2016 +0100
@@ -67,7 +67,7 @@
year, because Isabelle now includes its own version of Java, but the solution
back then was to replace
- exec "$ISABELLE_TOOL" java
+ exec isabelle java
in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Thu Mar 10 17:30:04 2016 +0100
@@ -118,7 +118,7 @@
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
- "$ISABELLE_TOOL" process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+ isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
}
function cleanup_workdir()
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Thu Mar 10 17:30:04 2016 +0100
@@ -30,5 +30,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Thu Mar 10 17:30:04 2016 +0100
@@ -28,4 +28,4 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-"$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
--- a/src/Pure/Thy/present.ML Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Pure/Thy/present.ML Thu Mar 10 17:30:04 2016 +0100
@@ -215,7 +215,7 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
- val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+ val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
val _ = if verbose then writeln s else ();
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Mar 10 17:30:04 2016 +0100
@@ -209,7 +209,7 @@
## dependencies
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- "$ISABELLE_TOOL" browser -b || exit $?
+ isabelle browser -b || exit $?
"$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
fi
@@ -361,5 +361,5 @@
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
classpath "$JEDIT_HOME/dist/jedit.jar"
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+ exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi
--- a/src/Tools/jEdit/lib/Tools/jedit_client Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit_client Thu Mar 10 17:30:04 2016 +0100
@@ -104,11 +104,11 @@
exit
fi
-"$ISABELLE_TOOL" jedit -b || exit $?
+isabelle jedit -b || exit $?
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
then
- exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
+ exec isabelle java "${JAVA_ARGS[@]}" \
-jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \
"-settings=$(platform_path "$JEDIT_SETTINGS")" \
-server="$SERVER_NAME" -reuseview "${ARGS[@]}"
--- a/src/Tools/jEdit/src/active.scala Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala Thu Mar 10 17:30:04 2016 +0100
@@ -33,7 +33,7 @@
Standard_Thread.fork("browser") {
val graph_file = Isabelle_System.tmp_file("graph")
File.write(graph_file, XML.content(body))
- Isabelle_System.bash("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
+ Isabelle_System.bash("isabelle browser -c \"$GRAPH_FILE\" &",
env = Map("GRAPH_FILE" -> File.standard_path(graph_file)))
}