From dc10b72ac7a28255f1ede1ca8001aa63191fd71b Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Thu, 26 Sep 2024 16:00:53 +0200 Subject: [PATCH] do not fail when goal as no loc when stack_trace is enabled --- src/session/itp_server.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index 821a90fa6..6be38b013 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -532,9 +532,10 @@ let get_locations (task: Task.task) = | None -> (* This case can happen when after some transformations: for example, in an assert, the new goal asserted is not tagged with locations *) - (* This error is harmless but we want to detect it when debugging. *) - if Debug.test_flag Debug.stack_trace then - raise No_loc_on_goal + (* This error is harmless but we want to detect it when debugging. *) + (* UPDATE: this is an annoying behavior when stack_trace is enabled *) + () (* if Debug.test_flag Debug.stack_trace then + raise No_loc_on_goal *) | Some loc -> color_loc ~color:Goal_color ~loc in let goal_id : Ident.ident = (Task.task_goal task).Decl.pr_name in color_goal goal_id.Ident.id_loc; -- 2.11.4.GIT