equal
deleted
inserted
replaced
74 #ML_SUFFIX=".psv" |
74 #ML_SUFFIX=".psv" |
75 #ML_PLATFORM="" |
75 #ML_PLATFORM="" |
76 |
76 |
77 |
77 |
78 ### |
78 ### |
79 ### Compilation options (cf. isatool usedir) |
79 ### Interactive sessions (cf. isatool tty) |
|
80 ### |
|
81 |
|
82 ISABELLE_LINE_EDITOR="" |
|
83 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" |
|
84 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" |
|
85 |
|
86 |
|
87 ### |
|
88 ### Batch sessions (cf. isatool usedir) |
80 ### |
89 ### |
81 |
90 |
82 ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML" |
91 ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML" |
83 |
92 |
84 # Specifically for the HOL image |
93 # Specifically for the HOL image |