116 |
116 |
117 val getopts = Getopts(""" |
117 val getopts = Getopts(""" |
118 Usage: isabelle process [OPTIONS] |
118 Usage: isabelle process [OPTIONS] |
119 |
119 |
120 Options are: |
120 Options are: |
|
121 -T THEORY load theory |
121 -d DIR include session directory |
122 -d DIR include session directory |
122 -e ML_EXPR evaluate ML expression on startup |
123 -e ML_EXPR evaluate ML expression on startup |
123 -f ML_FILE evaluate ML file on startup |
124 -f ML_FILE evaluate ML file on startup |
124 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
125 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
125 -m MODE add print mode for output |
126 -m MODE add print mode for output |
126 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
127 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
127 |
128 |
128 Run the raw Isabelle ML process in batch mode. |
129 Run the raw Isabelle ML process in batch mode. |
129 """, |
130 """, |
|
131 "T:" -> (arg => |
|
132 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), |
130 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
133 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
131 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
134 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
132 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
135 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
133 "l:" -> (arg => logic = arg), |
136 "l:" -> (arg => logic = arg), |
134 "m:" -> (arg => modes = arg :: modes), |
137 "m:" -> (arg => modes = arg :: modes), |