Undo, and the toolbar in three groups

Undo takes back one's own latest mark, by the button, Ctrl+Z or two
quick taps of the eraser; the toolbar's drawing tools, the page and
view, and the session stand in three groups that do not move when the
tool changes; the buttons are a little smaller.

docs/implementation.md

@@ -151,6 +151,17 @@ layer from that participant.  A client that reconnects after a dropped
 connection sends its whole layer again, so that nothing drawn meanwhile
 is lost.
 
+Undo is personal, since nobody can change another's layer, and is a
+stack of one's own gestures kept in the browser tab for the page being
+written: a stroke; the strokes and text blocks one movement of the
+eraser removed, kept whole; a text block as it was before an editing or
+a move; a Hide rectangle as it was before it was made, moved or removed.
+Undoing sends the ordinary messages, except that erased strokes come
+back by a `stroke_restore` message carrying them whole.  Images are not
+in the stack, because their data is not kept.  The stack is cleared when
+the page changes and is not in the page file, so a reloaded tab starts
+with nothing to undo.
+
 ## The page file
 
 A notebook is a directory.  The page being written is `Current.svg` in
@@ -264,7 +275,10 @@ by which the page grows (`page_model.js`), the tooltip delay
 slack, `pen_input.js`), the reach of an image's corner (24 pixels,
 `renderer.js`), the smallest an image can be scaled to (1 cm,
 `page_model.js`), how often a dragged image's place is sent (40 ms,
-`session.js`) and the points of a stroke (25 ms, `session.js`), the colour and width of a text rectangle's frame
+`session.js`) and the points of a stroke (25 ms, `session.js`), the
+interval of the eraser's double tap (400 ms, `DOUBLE_TAP_MS` in
+`main.js`) and how many gestures can be undone (100, `UNDO_LIMIT` in
+`session.js`), the colour and width of a text rectangle's frame
 (`page_file.js`) and whether the frame is shown whole or as corners on
 screen (`TEXT_FRAME_STYLE` in `renderer.js`; the file and the export
 always hold the whole frame).