[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Unicode TLA+
I think it could indeed be used to create a formatter. Say you wanted to write a rule where:
op == /\ A
/\ B
should be formatted as:
op ==
/\ A
/\ B
this would be quite easy; you would write a query for all operator definitions with conjunction lists as a top-level _expression_, so:
(operator_definition (def_eq) @eq definition: (conj_list) @list)
where the @eq capture gets the == node, and the @list capture gets the conjunction list node. Then you check whether the two nodes are on the same line (easy, info readily available in node object) and if so you insert a newline then dedent all lines included within the conjunction list node. This should preserve vertical alignment for any nested conjunction/disjunction lists.
Andrew
On Tuesday, September 14, 2021 at 2:49:23 PM UTC-4 Alexander Niederbühl wrote:
I think this would be very useful, I find the ASCII representation a bit verbose and distracting. I know of several people who feel the same, e.g. https://matklad.github.io/2020/11/01/notes-on-paxos.html as another data point. Currently I'm using a VSCode extension together with FiraCode as workaround.
A bit unrelated but since in TLA+ there are many ways to write the same thing like \cup, \union or /= , # and different ways to format the code in terms of line breaks etc. I wish there would be a tool to get a canonically formatted Unicode representation which ideally TLC would be able to check. Do you think the treesitter grammar could be utilized to build a code formatter similar to
prettier in _javascript_ or
black in Python?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/298f6ad5-90a0-408f-8f5d-0ca5814c0c19n%40googlegroups.com.