cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
225 stars 35 forks source link

alectryon.el: editing in reST mode should handle tabs #89

Open dunnl opened 1 year ago

dunnl commented 1 year ago

In alectryon.el, going from reST mode to Coq mode (or saving a file while opened in reST mode) does not handle tab characters that appear in coq blocks. Instead Alectryon seems to begin a new prose block.

Sample input (in reST mode). Note that auto here is indented with a hard tab character.

.. coq::

   Goal True.
   Proof.
    auto.
   Qed.

Sample output from saving or switching to Coq mode:

Goal True.
Proof.

(*|
    auto.
   Qed.
|*)

Output obtained if the tab is replaced with spaces:

Goal True.
Proof.
     auto.
Qed.
cpitclaudel commented 1 year ago

Ah, indeed — I haven't thought about tabs at all.

The reST spec says:

Spaces are recommended for indentation, but tabs may also be used. Tabs will be converted to spaces. Tab stops are at every 8th column (processing systems may make this value configurable).

How bad would it be to convert all tabs to spaces as part of the conversion process? Not exactly in line with the whole "reversible conversion" aspect, but very simple to implement ^^

cpitclaudel commented 1 year ago

I imagine the alternative would be to adjust the way the code measures indentation, but it will require in-depth testing to make sure that all cases are properly handled.

cpitclaudel commented 1 year ago

Ah, but this isn't sufficient, because dedenting a line may require replacing a tab with spaces before removing leading spaces. I will look into improving things, but given that tabs aren't used very commonly with reST, I'm curious to hear your thoughts on

How bad would it be to convert all tabs to spaces as part of the conversion process?

dunnl commented 1 year ago

I think that is reasonable. I encountered this issue when some editing I was doing silently inserted tab characters I didn't want.

cpitclaudel commented 1 year ago

Excellent. I will try to implement this.