search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
138 stars 25 forks source link

More interactive chat #82

Open joneugster opened 11 months ago

joneugster commented 11 months ago

It would be nice to have an option to show multiple small chat messages in sequence where the user has to click through them. This would avoid a massive text block.

Concretely: If there are multiple chat messages for a step, display the first one together with buttons "Next" and "Skip". These show, respectively, the next or all remaining chat messages

joneugster commented 1 month ago

New version features this for the intro text of a world and the game.

Implementing this I came to the conclusion - for now - that it probably wouldn't be preferable having to toggle messages whilst playing a level itself.

TentativeConvert commented 1 month ago

I like the new feature, and I agree that we don’t want this behaviour within levels. But I noticed two issues with this new feature:

Correcting what I wrote earlier, I do also see a specific narrow use for this within levels. Namely, the order in which the text within a level should be read is often:

  1. Read the level intro in the chat.
  2. Read the statement of the current exercise.
  3. Read the first hint.

It would make sense to hide the first hint (3.) until the player confirms they have read the actual statement (2.). Currently, it is simply unclear to the reader at which point they should move their focus to the statement of the exercise.

joneugster commented 1 month ago

(deleted, didnt read it properly. But I mostly agree with that)

joneugster commented 4 weeks ago

We might need to rethink what constitutes a “block” of text. From the intro of the NNG, I have the impression that (sub)headings are currently treated as separate blocks. They should be merged with the following paragraph.

Currently blocks are simply split by \n\s*\n (i.e. two consecutive line breaks) and I think this can be fixed in the NNG by simply removing line breaks at the correct place:

## More
Yada yada ...

instead of

## More

Yada yada ...

Is that good enough @TentativeConvert ?

Testing for this seprately is somewhat an annoyance because one would probably have to reiterate over all blocks and then merge them again depending on the starting symbol. But it's doable.

TentativeConvert commented 3 weeks ago

Is that good enough @TentativeConvert ?

Yes! That's most definitely good enough.