equal
deleted
inserted
replaced
13 { |
13 { |
14 echo |
14 echo |
15 echo "Usage: $PRG [OPTIONS]" |
15 echo "Usage: $PRG [OPTIONS]" |
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -g GEOM main window geometry (default 80x20)" |
18 # echo " -g GEOM main window geometry (default 80x20)" |
|
19 echo " (currently none)" |
19 echo |
20 echo |
20 echo " Starts Emacs and Isamode." |
21 echo "Starts Emacs and Isamode." |
21 echo |
|
22 exit 1 |
22 exit 1 |
23 } |
23 } |
24 |
24 |
25 function fail() |
25 function fail() |
26 { |
26 { |
31 |
31 |
32 ## process command line |
32 ## process command line |
33 |
33 |
34 # options |
34 # options |
35 |
35 |
36 MAINGEOM="80x20" |
36 #MAINGEOM="80x20" |
37 |
37 |
38 while getopts "g:" OPT |
38 #while getopts "g:" OPT |
39 do |
39 #do |
40 case "$OPT" in |
40 # case "$OPT" in |
41 g) |
41 # g) |
42 MAINGEOM="$OPTARG" |
42 # MAINGEOM="$OPTARG" |
43 ;; |
43 # ;; |
44 \?) |
44 # \?) |
45 usage |
45 # usage |
46 ;; |
46 # ;; |
47 esac |
47 # esac |
48 done |
48 #done |
49 |
49 |
50 shift $(($OPTIND - 1)) |
50 #shift $(($OPTIND - 1)) |
51 |
51 |
52 |
52 |
53 # args |
53 # args |
54 |
54 |
55 [ $# != 0 ] && usage |
55 [ $# != 0 ] && usage |
66 done |
66 done |
67 |
67 |
68 CMDS="$CMDS -f isabelle" |
68 CMDS="$CMDS -f isabelle" |
69 |
69 |
70 |
70 |
71 exec $ISAMODE_EMACS -T "Isabelle" -geometry $MAINGEOM $CMDS |
71 exec $ISAMODE_EMACS -T "Isabelle" $CMDS |
|
72 #exec $ISAMODE_EMACS -T "Isabelle" -geometry $MAINGEOM $CMDS |