minor tuning;
authorwenzelm
Tue, 07 Jan 1997 09:01:52 +0100
changeset 2474 9990f088d7ac
parent 2473 3eb12c85846c
child 2475 36bdba95e170
minor tuning;
lib/scripts/isa-emacs
lib/scripts/isa-xterm
src/Pure/mk
--- a/lib/scripts/isa-emacs	Tue Jan 07 09:01:18 1997 +0100
+++ b/lib/scripts/isa-emacs	Tue Jan 07 09:01:52 1997 +0100
@@ -18,4 +18,15 @@
 
 ## main
 
-exec emacs -name "isabelle" $ISABELLE_INTERFACE_OPTIONS -l "$ISAMODE_HOME/elisp/isa-site.el" -l "$ISABELLE_HOME_USER/etc/isa-settings.el" -l "$ISAMODE_HOME/elisp/isa-start.el"
+if [ -f "$ISABELLE_HOME_USER/etc/isa-settings.el" ]; then
+  USER_SETTINGS="--load $ISABELLE_HOME_USER/etc/isa-settings.el"
+else
+  USER_SETTINGS=""
+fi
+
+exec emacs -name "isabelle" \
+  --no-init-file $ISABELLE_INTERFACE_OPTIONS \
+  --load "$ISAMODE_HOME/elisp/isa-site.el" \
+  $USER_SETTINGS \
+  --load $HOME/.emacs \
+  --funcall isabelle
--- a/lib/scripts/isa-xterm	Tue Jan 07 09:01:18 1997 +0100
+++ b/lib/scripts/isa-xterm	Tue Jan 07 09:01:52 1997 +0100
@@ -18,9 +18,9 @@
 
 if [ -z "$ISABELLE_SYMBOLS" -o "$ISABELLE_SYMBOLS" = false ]; then
   exec xterm -T Isabelle -n Isabelle $ISABELLE_INTERFACE_OPTIONS \
-    -e $ISABELLE_HOME/bin/isabelle "$@"
+    -e $ISABELLE "$@"
 else
-  $ISABELLE_HOME/bin/isatool installfonts
+  $ISATOOL installfonts
   exec xterm -T Isabelle -n Isabelle $ISABELLE_INTERFACE_OPTIONS -fn isacr14 \
     -xrm "*fontMenu.Label: Isabelle fonts" \
     -xrm "*fontMenu*font1*Label: Large" \
@@ -35,5 +35,5 @@
     -xrm "*VT100*font5:" \
     -xrm "*fontMenu*font6*Label:" \
     -xrm "*VT100*font6:" \
-    -e $ISABELLE_HOME/bin/isabelle -e 'print_mode:=["symbols"];' "$@"
+    -e $ISABELLE -e 'print_mode:=["symbols"];' "$@"
 fi
--- a/src/Pure/mk	Tue Jan 07 09:01:18 1997 +0100
+++ b/src/Pure/mk	Tue Jan 07 09:01:52 1997 +0100
@@ -26,7 +26,7 @@
 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
 
-$ISABELLE_HOME/bin/isabelle \
+$ISABELLE \
   -e "val ml_system = \"$ML_SYSTEM\";" \
   -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
   -cq SYSTEM Pure