From d8ecc77eeaadb6a946b3f17e9aa7fc8570f0a6d2 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Dec 2004 20:31:24 +0000 Subject: [PATCH] ported to new format of Parse_error exception (which includes error position) --- helm/searchEngine/searchEngine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index f3e73af46..57c90f068 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -359,7 +359,7 @@ let callback dbd (req: Http_types.request) outchan = | Chat_unfinished -> () | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan - | CicTextualParser2.Parse_error msg -> + | CicTextualParser2.Parse_error (_, msg) -> send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan | Unbound_identifier id -> send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req -- 2.39.2