ported to new format of Parse_error exception (which includes error position)

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index f3e73af4686380a1a702b615aef30c05dec0dc4c..57c90f068272516aa6dc9889644500153194ea28 100644 (file)
--- 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