Method declarations in .ml files should link to their implementations

[jfehrle]

plugin version: 0.99-2021.1

source_buffer and the other declarations should have gutter icons linking to their implementations. Similarly, implementations should link back to their declarations.

[giraud]

Fixed in 0.108

[jfehrle]

Great, thanks! I noticed a tiny glitch: the very first time I open the .ml file I only see one gutter icon, like this:

then if I click on the gutter icon, it add icons on the detail items like this (rather than jumping to the mli file):

At that point it seems to be persistent, e.g. if I close and reopen the file and the project, all the icons are there immediately.

It would be cool to be able to jump from method clear : unit -> unit to the implementation (method clear () = buffer#set_text ""). Perhaps another day.

[giraud]

@jfehrle can you try with 0.113 ? code for gutter navigation has been rewritten

[jfehrle]

That addresses my Dec 1 comment above, thanks!

However, my original suggestion still applies: it would be great to have additional icons that link from the declaration in the .ml file to the implementation of each method. (The declaration could show both an up arrow icon and a down arrow icon in the gutter.)

[giraud]

@jfehrle I don’t know OCaml 'class type', can you point me where the implementation of 'proof_view' can be found ?

[jfehrle]

The file is available as https://github.com/coq/coq/blob/master/ide/coqide/wg_ProofView.ml. Note the class declaration in the file no longer exactly matches the image in the description.

refresh in the class declaration should link to:

  let pf = object(self)
     :
    method refresh ~force =    (* ON THIS LINE *)
     :
  end

[giraud]

thanks, I need to read more about objects and class types 😅