100 cleanup() |
100 cleanup() |
101 }) |
101 }) |
102 } |
102 } |
103 |
103 |
104 |
104 |
105 /* command line entry point */ |
105 /* Isabelle tool wrapper */ |
106 |
106 |
107 def main(args: Array[String]) |
107 val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => |
108 { |
108 { |
109 Command_Line.tool { |
109 var dirs: List[Path] = Nil |
110 var dirs: List[Path] = Nil |
110 var eval_args: List[String] = Nil |
111 var eval_args: List[String] = Nil |
111 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
112 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
112 var modes: List[String] = Nil |
113 var modes: List[String] = Nil |
113 var options = Options.init() |
114 var options = Options.init() |
|
115 |
114 |
116 val getopts = Getopts(""" |
115 val getopts = Getopts(""" |
117 Usage: isabelle process [OPTIONS] |
116 Usage: isabelle process [OPTIONS] |
118 |
117 |
119 Options are: |
118 Options are: |
120 -T THEORY load theory |
119 -T THEORY load theory |
121 -d DIR include session directory |
120 -d DIR include session directory |
125 -m MODE add print mode for output |
124 -m MODE add print mode for output |
126 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
125 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
127 |
126 |
128 Run the raw Isabelle ML process in batch mode. |
127 Run the raw Isabelle ML process in batch mode. |
129 """, |
128 """, |
130 "T:" -> (arg => |
129 "T:" -> (arg => |
131 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), |
130 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), |
132 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
131 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
133 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
132 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
134 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
133 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
135 "l:" -> (arg => logic = arg), |
134 "l:" -> (arg => logic = arg), |
136 "m:" -> (arg => modes = arg :: modes), |
135 "m:" -> (arg => modes = arg :: modes), |
137 "o:" -> (arg => options = options + arg)) |
136 "o:" -> (arg => options = options + arg)) |
138 |
137 |
139 val more_args = getopts(args) |
138 val more_args = getopts(args) |
140 if (args.isEmpty || !more_args.isEmpty) getopts.usage() |
139 if (args.isEmpty || !more_args.isEmpty) getopts.usage() |
141 |
140 |
142 ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). |
141 ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). |
143 result().print_stdout.rc |
142 result().print_stdout.rc |
144 } |
143 }) |
145 } |
|
146 } |
144 } |