From aa55e2ba934f681dbc7f835a687d46ebad96ff04 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Wed, 3 Jul 2024 20:01:23 +0200 Subject: [PATCH] [ide] use the editor configured in Why3 for the selected interactive prover --- src/plugins/wp/ProverWhy3.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml index ea4bc9329a4..b71a4378c18 100644 --- a/src/plugins/wp/ProverWhy3.ml +++ b/src/plugins/wp/ProverWhy3.ml @@ -1406,7 +1406,9 @@ let editor_mutex = Task.mutex () let editor_command pconf = let config = Why3Provers.config () in try - let ed = Why3.Whyconf.editor_by_id config pconf.Why3.Whyconf.editor in + let prover = pconf.Why3.Whyconf.prover in + let ed_id = Why3.Whyconf.get_prover_editor config prover in + let ed = Why3.Whyconf.editor_by_id config ed_id in String.concat " " (ed.editor_command :: ed.editor_options) with Not_found -> Why3.Whyconf.(default_editor (get_main config)) -- GitLab