- message (sprintf "execution of %s started:" fname);
- let script =
- let ic = open_in fname in
- let ast =
- try
- snd (CicTextualParser2.parse_script (Stream.of_channel ic))
- with
- exn ->
- error (explain exn);
- assert false (* should be something like (Unix.exit 1) *)
- in
- close_in ic;
- ast
- in
- let rec aux = function
- | [] -> () (* script is over *)
- | DisambiguateTypes.Comment _ :: tl -> aux tl
- | DisambiguateTypes.Command ast :: tl ->
- let loc =
- match ast with
- | TacticAst.LocatedTactical (loc, _) -> loc
- | _ -> assert false
- in
- let (success, _) = interpreter#evalAst ast in
- if not success then
- error (sprintf "%s: error at %s, aborting." fname
- (CicAst.pp_location loc))
- else
- aux tl