Getting Started with CalcCheckWeb

This page tries to help you getting started with the web interface aspects of CalcCheckWeb. For help with what to write into the boxes, see Getting Started with the CalcCheck Language.

1. There are two kinds of cells:
   • Code cells are displayed as a cell box containing two boxes, which are currently displayed side-by-side: The left box is the text entry area, and the right box shows CalcCheck output.

     Code cells are intended for the formal CalcCheck content.

   • MarkDown cells are displayed as a cell box containing just one box.

     MarkDown cells are intended for natural-language documentation and explanations.

     MarkDown cells either show the MarkDown source on a light green background in an entry box, or the generated HTML in a box that cannot be edited.

     Sending a source cell with Ctrl-ENTER generates HTML on the server, and then displays that.

2. Each cell is in one of the following two modes:
   • In edit mode, the cursor is active in the text area, and the text area is displayed in a lighter colour lighter than label to the left.
   • In command mode, the label to the left is lighter.
3. Clicking on a text entry area forces a cell into edit mode.
4. Clicking on the label to the left forces a cell into command mode.
5. If the current cell is in command mode, then the outer box has focus, and a slightly thicker line than the outer boxes of the other cells.

   Pressing the Enter key switches the current cell from command mode into edit mode.

6. If the current cell is in edit mode, then the text area has focus, and you have a cursor (or selection) there.

   Pressing the Esc key switches the current cell from edit mode into command mode.

7. The following key bindings work the same in both modes:

   Ctrl-Enter

   performs a syntax check on the contents of all code cells before and up to the current cell.

   Ctrl-Alt-Enter

   performs proof checks on the contents of all code cells before and up to the current cell.

   Alt-Shift-RightArrow

   enlarges the width of the current code cell entry area by a small amount

   Ctrl-Alt-Shift-RightArrow

   enlarges the width of the current code cell entry area by a large amount

   Alt-Shift-LeftArrow

   reduces the width of the current code cell entry area by a small amount

   Ctrl-Alt-Shift-LeftArrow

   reduces the width of the current code cell entry area by a large amount

   Ctrl-Shift-v

   (for visible spaces) toggles display of initial spaces on each line as “␣” characters.

   Ctrl-/

   splits the cell at the current cursor point.

   
   ONLY if you are logged in via Avenue:

   Ctrl-Shift-s

   saves the notebook on the server.

   (Links for reloading the last three saved versions are displayed when you load the notebook again later.)

   Ctrl-Alt-Shift-s

   Checks the whole notebook and saves it on the server.

   This is the same action that is triggered by the “Check and Save” button displayed at the end of the notebook.

8. In command mode, you have the following key bindings:

   Enter

   enters edit mode

   a

   inserts a code cell above the current cell

   A

   inserts a MarkDown cell above the current cell

   b

   inserts a code cell below the current cell

   B

   inserts a MarkDown cell below the current cell

   x

   clears the output area for current code cell

   Ctrl-x

   clears the output areas for all code cells

   d

   deletes the current cell, with a confirmation dialogue — there is no “undo”

   DownArrow

   shifts focus onto the next cell

   UpArrow

   shifts focus onto the previous cell

9. In edit mode, you have the following key bindings:

   Esc

   enters command mode.

   \

   brings up the symbol completion menu, see below.

   TAB

   If there is a left double quote (“) or a normal double quote character (") at least three characters to the left of the cursor, TAB performs theorem name completion, bringing up the theorem name completion menu if those characters are the start of more than one theorem name.

   If no theorem name completion applies, keyword completion is attempted instead.

   If the menu is brought up, it works essentially the same as for symbol completion (see below), except that the full menu is always visible, and backslash “\” switches to symbol completion inside the unfinished theorem name.

   Ctrl-b

   duplicates the two lines above the current cursor position.

   Alt-SPACE or Alt-i

   inserts one space in the current line and in all non-empty lines below it, until a line is encountered that is not indented more than to the cursor position.

   Alt-BACKSPACE

   deletes only a space character to the left of the current cursor position, and also from lines below it, until a line is encountered that is not indented at least to the cursor position.

   Alt-DELETE

   deletes only a space character to the right of the current cursor position, and also from lines below it, until a line is encountered that is not indented more than to the cursor position.

   The last three bindings also work with the Shift key pressed; at least on MSWindows and on some Ubuntu installations, this is necessary since Alt-SPACE is bound otherwise.
10. Completion menus are mostly “normal menus”, but continuing to type any key starting some options narrows down to only those options.

    More precisely, these menus can be controlled from the keyboard in the following way:

    “ESC”

    Removes the popup and the material typed so far, including the backslash (if it is still displayed) respectively double quote.

    “Ctrl-SPACE”

    Leaves the text in the current state, removing the popup.

    “ENTER”

    If the menu is displayed, uses the current selection; otherwise leaves the text in the current state, but adding a line break, removing the popup.

    “BACK_SPACE”

    Undoes the narrowing of options performed by the previously-typed character. If only the backslash had been typed, removes that and the popup.

    Key “k” from the options displayed between brackets “[ ]”:

    Narrows down to the options starting with k.

    Other key “k”:

    Removes the popup and leaves the text in the current state, also inserting k.

    “TAB”

    If an extension of the currently typed prefix is common to all still-active options, narrow down to the maximal such extension. The resulting new prefix is displayed at the top of the menu box.

    Otherwise, display the menu.

11. The symbol completion menu displays besides each symbol the sequence of characters to be input for obtaining it. For many symbols, their LaTeX macro is one of the possibilities.
12. Some standard functionality of your browser and/or windowing system will typically still be available, including:

    Ctrl-a

    selects all contents of current cell

    Ctrl-x

    cuts selected contents (to an internal clipboard)

    Ctrl-c

    copies selected contents (to the clipboard)

    Ctrl-v

    pastes the clipboard contents

13. If you are using the X11 window system (that is, essentially if you are on Linux or FreeBSD/PC-BSD/OpenBSD), you also have
    • selection by MouseLeft-down-and-drag
    • paste by MouseMiddle-click
14. Some important symbols (if this does not display correctly, choose Unicode (UTF-8) character encoding in your browser):

    Symbol	Key sequence(s)
    ⟨	\<, \langle, \beginhint
    ⟩	\>, \langle, \endhint
    “	\``, \ldquo
    ”	\'', \rdquo
    ·	\., \cdot
    ≤	\leq
    ≥	\geq
    𝔹	\BB, \bool
    ℕ	\NN, \nat
    ℤ	\ZZ, \int
    ℚ	\QQ, \rat
    ℝ	\RR, \real
    ℙ	\PP, \powerset
    ≡	\==, \equiv
    ≢	\nequiv
    ≠	\neq
    ≔	\becomes, \:=
    ¬	\lnot
    ∨	\lor
    ∧	\land
    ⇒	\implies, \=>
    ⇐	\follows, \<==
    —	\---
    ∀	\forall
    ∃	\exists
    ∑	\sum
    ∏	\product
    λ	\lambda, \Gl
    ❙	\with
    •	\spot
    ↓	\min
    ↑	\max
    ⁅	\[-
    ⁆	\]-
    ⍮	\;_
    ⟪	\<<
    ⟫	\>>
    ∈	\in
    ∪	\union
    ∩	\intersection
    ➩	\pseudocompl
    ⊆	\subseteq
    ⊂	\subset
    ⊇	\supseteq
    ⊃	\supset
    𝐔	\universe
    ×	\times
    ↔	\rel, <->
    ⦗	\lrel, \((, \([
    ⦘	\rrel, \)), \])
    ⨾	\rcomp, \fcomp, \;;
    ˘	\converse, \u{}
    ／	\lres
    ＼	\rres
    𝜖	\eps, \emptyseq
    ◃	\cons
    ▹	\snoc
    ⌢	\catenate

15. These special characters can be entered via character completion, see above.