Option to disable all of formatting (like subscript)

[ia0]

It would be nice if it were possible to disable all formatting in order to see the file we edit (syntax coloring is fine).

Most of the options may already be disabled (like prettify-symbols-mode and visual-line-mode), but the subscript formatting (like foo42 visualized as $foo_{42}$) currently cannot.

[cpitclaudel]

You can disable prettify-symbols-mode from fstar-enabled-modules.

I'm happy to add an option to disable subscripts. Are there other things? (Also, do you have examples of subscripts being a problem? They shouldn't hide anything from your buffer — they should just shift some text vertically)

[ia0]

Thanks for the fstar-enabled-modules. I configured it as I want and removed the redundant parts from my fstar-mode-hook. I just wonder what are fstar overlays and opinionated company-mode.

I still have one more query. If it would be possible to split the "Comment syntax and special comments" in two, "comment syntax" and "special comments", it would be great although not necessary. I don't use those special comments in my own code.

Other than that, the formatting looks pretty good to me.

The problem I have with subscripts (probably because I'm starting to be a dinosaur), is that it doesn't bring any visual help to me and the criteria looks pretty arbitrary. Why do something for foo42 and nothing for foo_42? I can imagine why people would benefit from forall to ∀ or other mathematical symbols, but I still prefer to have fixed space buffers, both horizontally and vertically. All in all, the only things that I find helpful without altering the actual file content, is syntax coloring (because it doesn't really affect the display, unless the foreground color is close to the background color) and the company completion (because it's an alteration which is limited in time: we know when it is active). Stuff like modeline (for type and documentation) is in a separate window so it's clearly limited in space: we know it's not part of the file.

And thanks for the mode! It's really helpful and nice to use. A good mix between proof general and company-style programming modes.

[cpitclaudel]

Noted, thanks for the clarification. I'll try to do the subscript thing soon.

When enabled, the Show a legend in the modeline when hovering an F* overlay option adds a hovertext to processed or in-processing code fragments, reminding you of the meaning of the various colors:

Opinionated company-mode configuration is a set of non-default settings for company-mode that work well with fstar-mode's backend:

(defun fstar-setup-company-defaults ()
  "…"
  (company-quickhelp-local-mode 1) ;; Shows docs in a popup
  (setq-local company-idle-delay 0.01) ;; Complete immediately
  (setq-local company-tooltip-align-annotations t) ;; Align annotations to the right
  (setq-local company-abort-manual-when-too-short t)) ;; Abort even manual completion on short prefixes, for performance reasons

[ia0]

Ok cool. Thanks for the explanations.

[cpitclaudel]

Done :)

[ia0]

Cool it works. I just needed to update the package. Thanks!