Formatting ASCII text

[Nick Radonic]

Is there a built in command to format/auto-indent the ASCII text? The "right-click + Format" looks like it is missing a sub-menu. In any case it does nothing.

I'm used to auto indentation in my IDE's .

Nick

========

I just loaded the environment last night. I've been reading about 'provably correct code' for years.

Thanks

[Leslie Lamport]

If you can write a precise specification (in English) of what a
"format/auto-indent" command should do, I will consider implementing
it.  However, be aware that incremental parsing of TLA+, or any
attempt to parse an incomplete spec, would be quite difficult and
anything requiring it will not be considered. 

 

This same offer applies to any other Toolbox editor command that
anyone thinks would be useful.

Meanwhile, you may want to experiment with the editing mode that
you get into and out of by typing Shift-Alt-A.

 

Leslie

[Nick Radonic]

A definition you say... therein lies the rub...

Hmm, still learning the names of things...

How about:

-State token (? ie. Next or Init) is aligned at column 1

-assignment operator "==" is  two spaces to right of state name

-arguments to assignment (i.e. IF, /\, \/)  are two columns right from assignment operator

-IF token is an argument to an assignment operator

-THEN token is two spaces to the right of the IF token, and on the next line after the IF arguments 

-ELSE token is two spaces to the right of the IF token, and on the next line after the THEN arguments

-token to token spacing would be a single space

Similar to:

SmallToBig == IF big + small <= 5

                THEN /\ big' = big + small

                    /\ small' = 0

                ELSE /\ big' = 5

                    /\ small' = small - (5 - big)

I would venture that your logic parser has a tree structure, and the indentation would roughly follow the tree level inside the parser.

Nick

[Nick Radonic]

Leslie

I kept watching videos on TLS+ and eventually found out about PlusCal. I also saw your videos from Stanford (6 rules for text alignment) and decided my original question was moot. I was looking for text editor behavior in a system that auto generated the TLS+ code.

Nick