# HG changeset patch # User wenzelm # Date 967830131 -7200 # Node ID 2be239143d422e16141a2fb006ab9cccbe26b6da # Parent 2c3d4e03e00c8b38613aa2046ab04808c792ec5b fixed quoting; diff -r 2c3d4e03e00c -r 2be239143d42 lib/Tools/browser --- a/lib/Tools/browser Fri Sep 01 19:40:57 2000 +0200 +++ b/lib/Tools/browser Fri Sep 01 19:42:11 2000 +0200 @@ -51,7 +51,11 @@ ## main export CLASSPATH="$ISABELLE_HOME/lib/browser" -[ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO" +if [ -z "$GRAPHFILE" ]; then + cd "$ISABELLE_BROWSER_INFO" + exec java GraphBrowser.GraphBrowser +else + java GraphBrowser.GraphBrowser "$GRAPHFILE" + [ -n "$DELETE" ] && rm -f "$GRAPHFILE" +fi -java GraphBrowser.GraphBrowser "$GRAPHFILE" -[ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE" diff -r 2c3d4e03e00c -r 2be239143d42 lib/scripts/isa-emacs --- a/lib/scripts/isa-emacs Fri Sep 01 19:40:57 2000 +0200 +++ b/lib/scripts/isa-emacs Fri Sep 01 19:42:11 2000 +0200 @@ -84,12 +84,12 @@ [ "$INITFILE" = false ] && ARGS="$ARGS -q" -ARGS="$ARGS -l \"$ISAMODE_HOME/elisp/isa-site.el\"" +ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el" for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \ "$ISABELLE_HOME_USER/etc/isa-settings.el" do - [ -f "$FILE" ] && ARGS="$ARGS -l \"$FILE\"" + [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" done ARGS="$ARGS -f isabelle" diff -r 2c3d4e03e00c -r 2be239143d42 lib/scripts/isa-xterm --- a/lib/scripts/isa-xterm Fri Sep 01 19:40:57 2000 +0200 +++ b/lib/scripts/isa-xterm Fri Sep 01 19:42:11 2000 +0200 @@ -104,7 +104,7 @@ PASS="$PASS_MODE $PASS" if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then - exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e \"$ISABELLE\" $PASS "$@" + exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e "$ISABELLE" $PASS "$@" else $ISATOOL installfonts exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \ @@ -121,5 +121,5 @@ -xrm "*VT100*font5:" \ -xrm "*fontMenu*font6*Label:" \ -xrm "*VT100*font6:" \ - -e \"$ISABELLE\" -m isabelle_font -m symbols $PASS "$@" + -e "$ISABELLE" -m isabelle_font -m symbols $PASS "$@" fi diff -r 2c3d4e03e00c -r 2be239143d42 lib/scripts/run-mosml --- a/lib/scripts/run-mosml Fri Sep 01 19:40:57 2000 +0200 +++ b/lib/scripts/run-mosml Fri Sep 01 19:42:11 2000 +0200 @@ -52,7 +52,7 @@ fi "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } + { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } RC="$?" [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"