equal
deleted
inserted
replaced
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 |