record stub

Stream: general

[Reid Barton]

The hole command to create a record stub is really nice!
Can any emacs gurus (@Simon Hudon?) tell me how I can write an emacs command that will insert {! !} at the point, navigate inside it (if necessary), and then invoke the Instance Stub hole command?

[Simon Hudon]

Sure :) Let's go step by step. In your configuration file (.emacs or .emacs.d/init.el), create a function, let's say:

(defun lean-insert-stub ()
  (print "hello world"))

[Simon Hudon]

You can change it a little so that you can invoke it from anywhere in emacs:

(defun lean-insert-stub ()
  (interactive)
  (print "hello world"))

Then, you just need M-x lean-insert-stub to invoke it.

[Simon Hudon]

And if you want it to actually do something:

(defun lean-insert-stub ()
  (interactive)
  (insert "{!  !}"))

[Reid Barton]

I tried having it call (lean-hole) next but I got an error even though repositioning the cursor after the insert isn't necessary interactively

[Reid Barton]

error in lean-server command handler: (wrong-type-argument number-or-marker-p nil)
Server response was:

[Simon Hudon]

I'm looking at lean-hole--command instead

[Reid Barton]

It kind of looks like the lean mode is not designed to handle selecting a hole command non-interactively, in terms of the code structure

[Reid Barton]

Am I supposed to locally set this thing completing-read-function? Is that the "emacs way"?

[Reid Barton]

not that that helps, when it is not getting that far yet

[Simon Hudon]

Yeah, now that I look more closely, it's not obvious

[Simon Hudon]

To be fair, I'm still new to emacs. Maybe @Sebastian Ullrich can shed some light. What I got so far is:

(defun lean-insert-stub ()
  (interactive)
  (insert "{!  !}")
  (forward-char -3)
  (let ((p (point)))
  (let ((start-pos p)
        (end-pos p))
    (let ((start-marker (make-marker))
          (end-marker (make-marker)))
      (set-marker start-marker start-pos (current-buffer))
      (set-marker end-marker end-pos (current-buffer))
      (lean-hole--command "Instance Stub" start-marker end-marker))))
  )

which I built from copying bits from lean-hole

[Jesse Michael Han]

i bound the first 3 lines of that command (just inserting the hole) to C-c C-SPC, do C-c SPC to open the menu, and tab-complete Ins

[Jesse Michael Han]

is the env <- get_env doing anything in the definition of instance_stub?

@[hole_command] meta def instance_stub : hole_command :=
{ name := "Instance Stub",
  descr := "Generate a skeleton for the structure under construction.",
  action := λ _,
  do tgt ← target >>= whnf,
     let cl := tgt.get_app_fn.const_name,
     env ← get_env,
     fs ← expanded_field_list cl,
     let fs := fs.map prod.snd,
     let fs := format.intercalate (",\n  " : format) $ fs.map (λ fn, format!"{fn} := _"),
     let out := format.to_string format!"{{ {fs} }",
     return [(out,"")] }

[Mario Carneiro]

looks vestigial to me