From f1c4fa3d9ba8dcf53d78e0aee5464e9b82347ae7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jun 2005 17:11:17 +0000 Subject: [PATCH] In case of EOI the "go ()" loop must exit! --- helm/matita/matitacLib.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 1f0aea715..d00156b8a 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -82,16 +82,20 @@ let pp_ocaml_mode () = MatitaLog.message "" let rec go () = + let str = Stream.of_channel stdin in try - run_script (Stream.of_channel stdin) MatitaEngine.eval_from_stream_greedy + run_script str MatitaEngine.eval_from_stream_greedy with | MatitaEngine.Drop -> pp_ocaml_mode () | Sys.Break -> MatitaLog.error "user break!"; go () | MatitaTypes.Command_error _ -> go () | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in - MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); - go () + (* check for EOI *) + if Stream.peek str = None then + exit 0 + else + let (x, y) = CicAst.loc_of_floc floc in + MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); | exn -> MatitaLog.error (Printexc.to_string exn); go () let main ~mode = -- 2.39.2