equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: console interaction for Isabelle server (with line-editor) |
5 # DESCRIPTION: console interaction for Isabelle servers (with line-editor) |
6 |
6 |
7 PRG="$(basename "$0")" |
7 PRG="$(basename "$0")" |
8 |
8 |
9 function usage() |
9 function usage() |
10 { |
10 { |
13 echo |
13 echo |
14 echo " Options are:" |
14 echo " Options are:" |
15 echo " -n NAME explicit server name" |
15 echo " -n NAME explicit server name" |
16 echo " -p PORT explicit server port" |
16 echo " -p PORT explicit server port" |
17 echo |
17 echo |
18 echo " Console interaction for Isabelle server (with line-editor)." |
18 echo " Console interaction for Isabelle servers (with line-editor)." |
19 echo |
19 echo |
20 exit 1 |
20 exit 1 |
21 } |
21 } |
22 |
22 |
23 function fail() |
23 function fail() |