fix(lsp): show success hints on the introducing keyword of commands and tactics

CHANGES.md

@@ -36,6 +36,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Fixed
 
+- A bare `open` (not preceded by `require`) was parsed as `require open`
+  since the parser rework, silently loading not yet required modules
+  instead of failing.
 - Convertibility test of non-linear higher-order pattern variables in rule LHS.
 - Syntactical errors in Dedukti export.
 - Weak head normal form test.
@@ -49,6 +52,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
   duplicated directory component.
 - LSP server: go-to-definition and hover on qualified identifiers, and session
   state leaking between open documents.
+- LSP server: the success ("OK") diagnostic of a command or tactic is now
+  shown on its introducing keyword ("symbol", "rule", "assume", …), instead
+  of underlining the whole command or tactic (symbol body, rule right-hand
+  side, proof, etc.).
 
 ## 3.0.0 (2025-07-16)
 

src/cli/lambdapi.ml

@@ -28,7 +28,8 @@ let sig_state_of_require l : Sig_state.sig_state =
     Handle.Command.handle Compile.compile ss
      (Pos.none
       (Parsing.Syntax.P_require
-        (Some false, [Pos.none (Parsing.Parser.path_of_string req)]))))
+        (Some false,
+         [Pos.none (Parsing.Parser.path_of_string req)]))))
   Core.Sig_state.dummy l
 
 let search_cmd cfg rules require s dbpath_opt =

src/common/pos.ml

@@ -111,6 +111,16 @@ let cat : popt -> popt -> popt = fun p1 p2 ->
   | None, Some p -> Some p
   | None, None -> None
 
+(** [prefix n p] is the sub-position of [p] covering only its first [n]
+    characters, which are assumed to lie on the first line of [p] and to be
+    ASCII (so that [n] is both a column count and a character count). *)
+let prefix : int -> popt -> popt = fun n p ->
+  match p with
+  | None -> None
+  | Some p -> Some { p with end_line = p.start_line
+                          ; end_col = p.start_col + n
+                          ; end_offset = p.start_offset + n }
+
 (** [shift k p] returns a position that is [k] characters after [p]. *)
 let shift : int -> popt -> popt = fun k p ->
   match p with

src/export/coq.ml

@@ -114,9 +114,9 @@ and typopt oc t = Option.iter (prefix " : " term oc) t
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(true,ps) ->
+  | P_open(_,true,ps) ->
       string oc "Import "; list path " " oc ps; string oc ".\n"
-  | P_open(false,ps) ->
+  | P_open(_,false,ps) ->
       string oc "Export "; list path " " oc ps; string oc ".\n"
   | P_require (None, ps) ->
       string oc "Require "; list path " " oc ps; string oc ".\n"
@@ -129,7 +129,7 @@ let command oc {elt; pos} =
     string oc "Module "; ident oc i; string oc " := "; path oc p;
     string oc ".\n"
   | P_symbol
-    { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+    { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
       p_sym_trm; p_sym_prf=_; p_sym_def } ->
       if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with

src/export/lean.ml

@@ -140,7 +140,7 @@ let openings = ref []
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(_,ps) -> List.iter (open_mod oc) ps
+  | P_open(_,_,ps) -> List.iter (open_mod oc) ps
   | P_require(b,ps) ->
       List.iter (req_mod oc) ps;
       begin
@@ -149,8 +149,8 @@ let command oc {elt; pos} =
         | _ -> () (*FIXME?*)
       end
   | P_require_as(p,i) -> Stt.alias := StrMap.add i.elt p.elt !Stt.alias
-  | P_symbol { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm;
-               p_sym_prf=_; p_sym_def } ->
+  | P_symbol { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
+               p_sym_trm; p_sym_prf=_; p_sym_def } ->
     if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with
           | true, Some t, _, Some a when List.exists is_lem p_sym_mod ->

src/export/rawdk.ml

@@ -198,7 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_query q -> query ppf q
   | P_require(None,ps) ->
       List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps
-  | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg; p_sym_typ;
+  | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ;
              p_sym_trm; p_sym_prf=None; p_sym_def=_;} ->
       let ms = partition_modifiers p_sym_mod in
       begin match get_ac_typ pos ms p_sym_arg p_sym_typ with

src/handle/command.ml

@@ -249,7 +249,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | P_require(bo,ps) ->
       (List.fold_left (handle_require compile bo) ss ps, None, None)
   | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None)
-  | P_open(b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
+  | P_open(_,b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
   | P_rules(rs) ->
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a [map] mapping every symbol defined by a rule
@@ -344,7 +344,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       Console.out 2 (Color.gre "coercion %a") sym_rule r;
       (ss, None, None)
 
-  | P_inductive(ms, params, p_ind_list) ->
+  | P_inductive(_, ms, params, p_ind_list) ->
       (* Check modifiers. *)
       let (prop, expo, mstrat, opaq) = handle_modifiers ms in
       if prop <> Defin then
@@ -446,8 +446,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         rec_sym_list;
       (ss, None, None)
 
-  | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;
-              p_sym_def} ->
+  | P_symbol {p_sym_mod;p_sym_kw=_;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;
+              p_sym_prf;p_sym_def} ->
     (* We check that the identifier is not already used. *)
     let {elt=id; _} = p_sym_nam in
     if Sign.mem ss.signature id then

src/lsp/lp_doc.ml

@@ -22,7 +22,7 @@ module LSP = Lsp_base
 let lp_logger = Buffer.create 100
 
 type doc_node =
-  { ast   : Pure.Command.t
+  { cmd   : Pure.Command.t
   ; exec  : bool
   (*; tactics : Proof.Tactic.t list*)
   ; goals : (Goal.info list * Pos.popt) list
@@ -63,7 +63,10 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
   | Tac_OK (pstate, qres) ->
     let goals = Some (current_goals pstate) in
     let qres = match qres with None -> "OK" | Some x -> x in
-    pstate, (tac_loc, 4, qres, goals) :: diags, logs
+    (* Show the success hint on the tactic's leading keyword only. This
+       tuple also anchors the goals panel (see [get_goals]), whose lookup
+       reads the start of the position: the start must not move. *)
+    pstate, (Tactic.keyword_pos tac, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
     let goals = Some (current_goals pstate) in
@@ -83,27 +86,32 @@ let get_goals dg_proof =
   in get_goals_aux [] dg_proof
 (* XXX: Imperative problem *)
 
-let process_cmd _file (nodes,st,dg,logs) ast =
+let process_cmd _file (nodes,st,dg,logs) cmd =
   let open Pure in
   (* let open Timed in *)
   (* XXX: Capture output *)
   (* Console.out_fmt := lp_fmt;
    * Console.err_fmt := lp_fmt; *)
-  let cmd_loc = Command.get_pos ast in
-  let hndl_cmd_res = handle_command st ast in
+  let cmd_loc = Command.get_pos cmd in
+  let hndl_cmd_res = handle_command st cmd in
   let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in
   match hndl_cmd_res with
   | Cmd_OK (st, qres) ->
     let qres = match qres with None -> "OK" | Some x -> x in
-    let nodes = { ast; exec = true; goals = [] } :: nodes in
-    let ok_diag = cmd_loc, 4, qres, None in
+    let nodes = { cmd; exec = true; goals = [] } :: nodes in
+    (* Show the success hint on the command's introducing keyword only. *)
+    let ok_diag = Command.keyword_pos cmd, 4, qres, None in
     nodes, st, ok_diag :: dg, logs
   | Cmd_Proof (pst, tlist, thm_loc, qed_loc) ->
     let start_goals = current_goals pst in
     let pst, dg_proof, logs = process_proof pst tlist logs in
-    let dg_proof = (thm_loc, 4, "OK", Some start_goals) :: dg_proof in
-    let goals = get_goals dg_proof in
-    let nodes = { ast; exec = true; goals } :: nodes in
+    (* Initial goals stay anchored at the symbol, for the goals panel. *)
+    let goals =
+      get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in
+    let nodes = { cmd; exec = true; goals } :: nodes in
+    (* Visible success hint on the "symbol" keyword, not on the symbol
+       name. *)
+    let dg_proof = (Command.keyword_pos cmd, 4, "OK", None) :: dg_proof in
     let st, dg_proof, logs =
       match end_proof pst with
       | Cmd_OK (st, qres)   ->
@@ -123,7 +131,7 @@ let process_cmd _file (nodes,st,dg,logs) ast =
     nodes, st, dg_proof @ dg, logs
 
   | Cmd_Error(loc, msg) ->
-    let nodes = { ast; exec = false; goals = [] } :: nodes in
+    let nodes = { cmd; exec = false; goals = [] } :: nodes in
     let cmd_loc, loc, diag, log = match cmd_loc, loc with
     | Some l, Some Some l' ->
         if l.fname = l'.fname then

src/lsp/lp_lsp.ml

@@ -222,8 +222,8 @@ let in_range ?loc (line, pos) =
 
 let get_node_at_pos doc line pos =
   let open Lp_doc in
-  List.find_opt (fun { ast; _ } ->
-      let loc = Pure.Command.get_pos ast in
+  List.find_opt (fun { cmd; _ } ->
+      let loc = Pure.Command.get_pos cmd in
       in_range ?loc (line,pos)
     ) doc.Lp_doc.nodes
 

src/parsing/dkParser.mly

@@ -49,6 +49,7 @@
     let symbol lps p_sym_mod i ps p_sym_typ p_sym_trm =
       make_pos lps (P_symbol
         { p_sym_mod
+        ; p_sym_kw = None (* Dedukti has no "symbol" keyword. *)
         ; p_sym_nam = p_ident i
         ; p_sym_arg = List.map (fun (i,t) -> params i (Some t)) ps
         ; p_sym_typ
@@ -77,7 +78,8 @@
 
     let query lps q = make_pos lps (P_query q)
 
-    let require (lps,id) = make_pos lps (P_require(None,[make_pos lps [id]]))
+    let require (lps,id) =
+      make_pos lps (P_require(None,[make_pos lps [id]]))
 
     let arrow lps a b = make_pos lps (P_Arro (a, b))
     let binary lps a = arrow lps a (arrow lps a a)

src/parsing/lpParser.ml

@@ -433,14 +433,23 @@ let term_id (lb:'token lexbuf): p_term =
 
 (* commands *)
 
-let open_ (priv:bool) (lb:'token lexbuf) : p_command_aux =
+(* [req] tells whether the command starts with the [require] keyword:
+   [require [private] open] loads the modules and opens them
+   ([P_require]), while a bare [[private] open] only opens modules
+   that are already loaded ([P_open]). For a bare open, the position
+   of the "open" keyword is recorded in the AST (a "private" modifier,
+   like modifiers of symbol declarations, is not part of the
+   keyword). *)
+let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux =
  if log_enabled() then log "%s" __FUNCTION__;
+ let kw_pos = Some(locate (current_pos lb)) in
  consume OPEN lb;
  let ps = nelist path_tks path lb in
- P_require(Some priv,ps)
+ if req then P_require(Some priv,ps) else P_open(kw_pos,priv,ps)
 
 let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
  if log_enabled() then log "%s" __FUNCTION__;
+ let p_sym_kw = Some(locate (current_pos lb)) in
  consume SYMBOL lb;
  let p_sym_nam = uid lb in
  let p_sym_arg = list params_tks params lb in
@@ -456,23 +465,23 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
              let p_sym_prf = Some (proof lb) in
              let p_sym_def = false in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm=None; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | ASSIGN ->
              consume_token lb;
              let p_sym_trm, p_sym_prf = term_proof lb in
              let p_sym_def = true in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | SEMICOLON ->
              let p_sym_trm = None in
              let p_sym_def = false in
              let p_sym_prf = None in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | _ ->
@@ -484,7 +493,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
        let p_sym_def = true in
        let p_sym_typ = None in
        let sym =
-         {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+         {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
           p_sym_trm; p_sym_def; p_sym_prf}
        in P_symbol(sym)
    | _ ->
@@ -497,10 +506,11 @@ and inductive_cmd (p_sym_mod:p_modifier list) (lb:'token lexbuf)
  let xs = list params_tks params lb in
  match current_token lb with
  | INDUCTIVE ->
+     let kw_pos = Some(locate (current_pos lb)) in
      consume INDUCTIVE lb;
      let i = inductive lb in
      let is = list [WITH] (prefix WITH inductive) lb in
-     P_inductive(p_sym_mod,xs,i::is)
+     P_inductive(kw_pos,p_sym_mod,xs,i::is)
  | _ -> expected lb "" [L_PAREN;L_SQ_BRACKET;INDUCTIVE]
 
 and command (lb:'token lexbuf) : p_command =
@@ -520,7 +530,7 @@ and command (lb:'token lexbuf) : p_command =
     end
  | [{elt=P_expo Term.Privat;_}] ->
     begin match current_token lb with
-    | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb)
+    | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ false true lb)
     | SYMBOL ->
         extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb)
     | L_PAREN
@@ -546,10 +556,10 @@ and command (lb:'token lexbuf) : p_command =
         begin
           match current_token lb with
           | OPEN ->
-              extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb)
+              extend_pos lb (*__FUNCTION__*) pos1 (open_ true false lb)
           | PRIVATE ->
               consume_token lb;
-              extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb)
+              extend_pos lb (*__FUNCTION__*) pos1 (open_ true true lb)
           | QID _ ->
               let ps = nelist path_tks path lb in
               begin
@@ -565,12 +575,13 @@ and command (lb:'token lexbuf) : p_command =
                     extend_pos lb (*__FUNCTION__*) pos1 (P_require_as(p,i))
                 | _ ->
                     set_expected_tokens lb [AS] ;
-                    extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps))
+                    extend_pos lb (*__FUNCTION__*) pos1
+                      (P_require(None,ps))
               end
           | _ -> expected lb "" [OPEN;PRIVATE;QID[]]
         end
     | OPEN ->
-        extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb)
+        extend_pos lb (*__FUNCTION__*) pos1 (open_ false false lb)
     | SYMBOL ->
         extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb)
     | L_PAREN

src/parsing/parser.ml

@@ -75,7 +75,7 @@ module Dk : PARSER with type lexbuf := Lexing.lexbuf = struct
     parse_lexbuf None entry lb
 
   let command =
-    let r = ref (Pos.none (P_open(false,[]))) in
+    let r = ref (Pos.none (P_open(None,false,[]))) in
     fun (lb:lexbuf): p_command ->
     Debug.(record_time Parsing
              (fun () -> r := DkParser.line DkLexer.token lb)); !r

src/parsing/pretty.ml

@@ -367,16 +367,16 @@ let proof : (p_proof * p_proof_end) pp = fun ppf (p, pe) ->
 let command : p_command pp = fun ppf { elt; _ } ->
   begin match elt with
   | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid
-  | P_inductive (_, _, []) -> assert false (* not possible *)
-  | P_inductive (ms, xs, i :: il) ->
+  | P_inductive (_, _, _, []) -> assert false (* not possible *)
+  | P_inductive (_, ms, xs, i :: il) ->
     let with_ind ppf i = out ppf "@,%a" (inductive "with") i in
     out ppf "@[<v>@[%a%a@]%a%a@]"
       modifiers ms (List.pp params " ") xs
       (inductive "inductive") i (List.pp with_ind "") il
   | P_notation (qid, n) ->
     out ppf "notation %a %a" qident qid (Print.notation string) n
-  | P_open(false,ps) -> out ppf "open %a" (List.pp path " ") ps
-  | P_open(true,ps) -> out ppf "private open %a" (List.pp path " ") ps
+  | P_open(_,false,ps) -> out ppf "open %a" (List.pp path " ") ps
+  | P_open(_,true,ps) -> out ppf "private open %a" (List.pp path " ") ps
   | P_query q -> query ppf q
   | P_require (None, ps) -> out ppf "require %a" (List.pp path " ") ps
   | P_require (Some false, ps) ->
@@ -389,7 +389,7 @@ let command : p_command pp = fun ppf { elt; _ } ->
     let with_rule ppf r = out ppf "@.%a" (rule "with") r in
     rule "rule" ppf r; List.iter (with_rule ppf) rs
   | P_symbol
-    { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+    { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
       p_sym_trm; p_sym_prf; p_sym_def } ->
     begin
       out ppf "@[<v>@[<2>%asymbol %a%a%a%a%a@]%a@]"