lib/scripts/isa-xterm
changeset 9794 2be239143d42
parent 9789 7e5e6c47c0b5
child 10512 d34192966cd8
equal deleted inserted replaced
9793:2c3d4e03e00c 9794:2be239143d42
   102 fi
   102 fi
   103 
   103 
   104 PASS="$PASS_MODE $PASS"
   104 PASS="$PASS_MODE $PASS"
   105 
   105 
   106 if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
   106 if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
   107   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e \"$ISABELLE\" $PASS "$@"
   107   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e "$ISABELLE" $PASS "$@"
   108 else
   108 else
   109   $ISATOOL installfonts
   109   $ISATOOL installfonts
   110   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
   110   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
   111     -xrm "*fontMenu.Label: Isabelle fonts" \
   111     -xrm "*fontMenu.Label: Isabelle fonts" \
   112     -xrm "*fontMenu*font1*Label: Large" \
   112     -xrm "*fontMenu*font1*Label: Large" \
   119     -xrm "*VT100*font4:" \
   119     -xrm "*VT100*font4:" \
   120     -xrm "*fontMenu*font5*Label:" \
   120     -xrm "*fontMenu*font5*Label:" \
   121     -xrm "*VT100*font5:" \
   121     -xrm "*VT100*font5:" \
   122     -xrm "*fontMenu*font6*Label:" \
   122     -xrm "*fontMenu*font6*Label:" \
   123     -xrm "*VT100*font6:" \
   123     -xrm "*VT100*font6:" \
   124     -e \"$ISABELLE\" -m isabelle_font -m symbols $PASS "$@"
   124     -e "$ISABELLE" -m isabelle_font -m symbols $PASS "$@"
   125 fi
   125 fi