diff --git a/base-packages.lisp b/base-packages.lisp
index 05d0068..844bfcd 100644
--- a/base-packages.lisp
+++ b/base-packages.lisp
@@ -7,6 +7,11 @@
    #:delim-p
    #:symbol-char-p
    #:proposition-parse-error
+   #:parse-error-position
+   #:parse-error-proposition
+   #:parse-error-message
+   #:*operator-symbol-table*
+   #:*operator-descriptions*
    #:operator-symbol
    #:operator-precedence
    #:interpret-operand
@@ -45,6 +50,7 @@
    #:convert-truth-table-to-html
    #:*table-border-ascii-alist*
    #:*table-border-unicode-alist*
+   #:with-draw-table
    #:typeset-truth-table
    #:*known-formats*
    #:typeset-table-to-format))
diff --git a/cli.lisp b/cli.lisp
index fc895e4..fa6a260 100644
--- a/cli.lisp
+++ b/cli.lisp
@@ -50,8 +50,80 @@ functions involved in evaluating and typesetting."
                                               :pretty-print pretty-print
                                               :latin-truths latin-truths)))))
 
+(defun word-wrap-string (string &optional (cols 80))
+  (with-output-to-string (str)
+    (loop with word = ()
+          with word-len = 0
+          with cur-col = 0
+          for char across string
+          when (whitespace-p char) do
+            (if (>= (+ cur-col word-len 1) cols)
+                (progn
+                  (terpri str)
+                  (setq cur-col 0))
+                (unless (zerop cur-col)
+                  (format str " ")
+                  (incf cur-col)))
+            (format str "~{~c~}" (nreverse  word))
+            (setq word nil
+                  cur-col (+ cur-col word-len)
+                  word-len 0)
+          else do
+            (push char word)
+            (incf word-len)
+          finally
+             (if (>= (+ cur-col word-len 1) cols)
+                 (terpri str)
+                 (format str " "))
+             (format str "~{~c~}" (nreverse word)))))
+
+(defun ascii-string-p (str)
+  "Return true if STR is only ASCII characters."
+  (loop for char across str
+        unless (<= (char-code char) 127)
+          do (return-from ascii-string-p))
+  t)
+
+(defun print-syntax-help (ascii-only)
+  "Print the syntax help message."
+  (loop
+    for ((sym (name . nicks) desc examples) . rest-desc)
+      = *operator-descriptions* then rest-desc
+    for ((_sym . syntax) . rest-st) = *operator-symbol-table* then rest-st
+    for syntax-str = (format nil "~{~a~^, ~}"
+                             (sort (copy-list
+                                    (if ascii-only
+                                        (remove-if-not 'ascii-string-p
+                                                       syntax)
+                                        syntax))
+                                   'string<))
+    while sym
+    maximize (length name) into name-col-len
+    maximize (length syntax-str) into syntax-col-len
+    collect syntax-str into syntax-entries
+    finally
+       (let ((col-widths (list name-col-len syntax-col-len))
+             (box-lookup-table (if ascii-only
+                                   *table-border-ascii-alist*
+                                   *table-border-unicode-alist*)))
+         (with-draw-table (t col-widths box-lookup-table
+                           :padding 1 :align :left)
+           (:row (list "Operator" "Syntax"))
+           (:seperator)
+           (loop for (sym (name . nicks) desct) in *operator-descriptions*
+                 for syntax-str in syntax-entries do
+                   (:row (list name syntax-str))))))
+  (format t "~%~%~a~%Example:~%  abc|d = ~a~%"
+          (word-wrap-string "Two operands next to each other is treated as an
+'implicit and' (unless this feature is disabled).")
+          (typeset-proposition '(or (and "a" "b" "c") "d")
+                               :lookup-table (if ascii-only
+                                                 *operator-ascii-lookup-alist*
+                                                 *operator-unicode-lookup-alist*))))
+
 (defparameter *command-line-spec*
   '((#\h "help" help nil "print this message, then exit")
+    (nil "syntax-help" syntax-help nil "print a syntax help message, then exit")
     (#\f "format" format t
      "specify the output format (*unicode*, ascii, latex, or html)")
     (#\s "subexps" subexps nil "include sub-expressions in the output table")
@@ -85,6 +157,20 @@ arguments."
            (print-usage t *command-line-spec* "truth-table"
                         :general-args "<propositions...>")
            (uiop:quit (if cmdline-error 1 0)))
+          ((and (not cmdline-error) ;; if option parsing failed, error out
+                (option-value 'syntax-help opts))
+           (let ((format (option-value 'format opts)))
+             (cond
+               ((or (not format)
+                    (equal format "unicode"))
+                (print-syntax-help nil))
+               ((equal format "ascii")
+                (print-syntax-help t))
+               (t
+                (cerror "Exit without printing anything" 'command-line-error
+                        :message (format nil "The syntax help table is only ~
+                       available in ASCII or Unicode.")))))
+           (uiop:quit))
           ((null prop-strs)
            (cerror *cli-parse-continue-string* 'no-input-error))
           (cmdline-error
@@ -96,12 +182,12 @@ arguments."
                (setq format "unicode"))
              (princ (eval-and-typeset-propositions
                      prop-strs :format format
-                               :implicit-and (not (option-value 'no-implicit opts))
-                               :multi-char-names (option-value 'multi-char opts)
-                               :include-vars (not (option-value 'no-vars opts))
-                               :include-intermediate (option-value 'subexps opts)
-                               :pretty-print (option-value 'pretty opts)
-                               :latin-truths (option-value 'latin opts)))
+                     :implicit-and (not (option-value 'no-implicit opts))
+                     :multi-char-names (option-value 'multi-char opts)
+                     :include-vars (not (option-value 'no-vars opts))
+                     :include-intermediate (option-value 'subexps opts)
+                     :pretty-print (option-value 'pretty opts)
+                     :latin-truths (option-value 'latin opts)))
              (terpri))))))))
 
 (defun toplevel ()
diff --git a/parse.lisp b/parse.lisp
index 74ae3cb..035c0f4 100644
--- a/parse.lisp
+++ b/parse.lisp
@@ -86,6 +86,77 @@ proposition."))
     (iff "<->" "<>" "<=>" "⇔" "↔" "≡" "iff" "=" "==" "xnor" "⊙"))
   "Alist table of operator symbols and their possible string representations.")
 
+(defparameter *operator-descriptions* ;; noindent 30
+  `((open-paren ("open parenthesis")
+     ,(format nil "Used in combination with a close parenthesis to denote ~
+some terms to be evaluated before the surrounding terms.")
+     (((and (or true true) false) . false)
+      ((or true (and true false)) . true)))
+    (close-paren ("close parenthesis")
+     "Used to close a group started with an open parenthesis."
+     ()) ;; no examples for closed paren
+    (and ("and" "conjunction")
+     ,(format nil "Evaluate to true only if the expressions to the left and ~
+right evaluate to true.")
+     (((and true true) . true)
+      ((and true false) . false)))
+    (nand ("nand" "non-conjunction")
+     ,(format nil "Evaluate to true unless the expressions to the left and ~
+right are both true. This is the negation of the 'and' operator.")
+     (((nand true true) . false)
+      ((nand true false) . true)
+      ((nand false false) . true)))
+    (or ("or" "disjunction")
+     ,(format nil "Evaluate to true if the expression to the left is true, the ~
+expression to the right is true, or both the left and right expressions are ~
+true.")
+     (((or true true) . true)
+      ((or true false) . true)
+      ((or false false) . false)))
+    (nor ("nor" "non-disjunction")
+     ,(format nil "Evaluate to true if the expressions to the left and right ~
+are both false. This is the negation of the 'or' operator.")
+     (((nor true true) . false)
+      ((nor true false) . false)
+      ((nor false false) . true)))
+    (xor ("exclusive or" "exclusive disjunction") ;; noindent 30
+     ,(format nil "Evaluate to true if the expression to the left is true or ~
+if the expression to the right is true, but not if both of them are true.")
+     (((xor true true) . false)
+      ((xor true false) . true)))
+    (not ("not" "negation")
+     ,(format nil "Evaluate to false if the expression to the left evaluates ~
+to true, and evaluate to true if the expression to the left evaluates to ~
+false. This is a unary operator (it only applies to the expression following ~
+it).")
+     (((not true) . false)
+      ((not false) . true)))
+    (implies ("implies" "conditional")
+     ,(format nil "Evaluate to false if the expression to the left evaluates ~
+to true and the expressions to the right evaluates to false. Otherwise, ~
+evaluate to true.")
+     (((implies true true) . true)
+      ((implies true false) . false)
+      ((implies false true) . true)
+      ((implies false false) . true)))
+    (converse ("converse")
+     ,(format nil "Evaluate to false if the expression to the right evaluates ~
+to true and the expression to the left evaluates to false. Otherwise, evaluate ~
+to true. This is the 'implies' operator with its arguments flipped.")
+     (((implies true true) . true)
+      ((implies true false) . true)
+      ((implies false true) . false)
+      ((implies false false) . true)))
+    (iff ("biconditional" "equivalent")
+     ,(format nil "Evaluate to true if the expressions to the left and rigt ~
+evaluate to the same value. That is, they are both true or both false.")
+     (((iff true true) . true)
+      ((iff true false) . false)
+      ((iff false false) . true))))
+  "Alist table of operator symbols and their descriptions. The format of this
+list is SYMBOL NAMES DESCRIPTION (&rest (EXAMPLE LEFT . EXAMPLE RIGHT)). These
+are useful for use in things like syntax explanation messages.")
+
 (defun operator-symbol (oper-str)
   "Return the symbol for OPER-STR, or nil if it is not a know operator."
   (loop for (oper-sym . strs) in *operator-symbol-table*
diff --git a/typeset.lisp b/typeset.lisp
index eeb7659..c369bbb 100644
--- a/typeset.lisp
+++ b/typeset.lisp
@@ -318,7 +318,8 @@ between each row."
     (bottom-right . #\┘))
   "Characters used to draw Unicode table borders.")
 
-(defun typeset-table-break (stream lengths horiz start column end)
+(defun typeset-table-break (stream lengths horiz start column end
+                            &key (left-pad-len 0) (right-pad-len 0))
   "Typeset the first row, the last row, or a break to STREAM. The proper box
 character will be placed at each intersection. LENGTHS is a list of column
 lengths. HORIZ, START, COLUMN, and END are the box characters to use when
@@ -328,20 +329,78 @@ drawing."
         while length
         do
            (format stream "~a"
-                   (make-string length :initial-element horiz))
+                   (make-string (+ left-pad-len length right-pad-len)
+                                :initial-element horiz))
         when rest do
           (format stream "~c" column))
   (format stream "~c" end))
 
-(defun typeset-table-row (stream lengths row vert)
+(defun typeset-table-row (stream lengths row vert
+                          &key (align :center) (left-pad-str "")
+                            (right-pad-str ""))
   "Typeset ROW to STREAM. VERT is the vertical separator. LENGTHS should be the
 length of each column."
-  (loop for col in row
+  (loop with format = (case align
+                        (:right
+                         "~c~a~v:<~a~>~a")
+                        (:left
+                         "~c~a~v@<~a~>~a")
+                        (t ;; :center
+                         "~c~a~v:@<~a~>~a"))
+        for col in row
         for length in lengths
         do
-           (format stream "~c~v:@<~a~>" vert length col))
+           (format stream format
+                   vert left-pad-str length col right-pad-str))
   (format stream "~c" vert))
 
+(defmacro with-draw-table ((stream col-widths lookup-table
+                            &key (padding 0) (align :center))
+                           &body body)
+  "Execute BODY with the function \=:seperator and \=:row bound. STREAM is the
+stream to write the table to. COL-WIDTHS is a list of column
+widths. LOOKUP-TABLE is the table to use to lookup characters for the table
+border. PADDING is the number to spaces to both append and prepend to each table
+cell. ALIGN is one of \=:right, \=:center, or \=:left."
+  (let ((pad-str-var (gensym)))
+    `(let ((,pad-str-var (make-string ,padding :initial-element #\space)))
+       (truth-table/base::typeset-table-break
+        ,stream ,col-widths
+        (cdr (assoc 'horizontal ,lookup-table))
+        (cdr (assoc 'top-left ,lookup-table))
+        (cdr (assoc 'down ,lookup-table))
+        (cdr (assoc 'top-right ,lookup-table))
+        :right-pad-len ,padding
+        :left-pad-len ,padding)
+       (format ,stream "~%")
+       (flet ((:seperator ()
+               (truth-table/base::typeset-table-break
+                ,stream ,col-widths
+                (cdr (assoc 'horizontal ,lookup-table))
+                (cdr (assoc 'right ,lookup-table))
+                (cdr (assoc 'cross ,lookup-table))
+                (cdr (assoc 'left ,lookup-table))
+                :right-pad-len ,padding
+                :left-pad-len ,padding)
+               (format ,stream "~%"))
+              (:row (row)
+               (truth-table/base::typeset-table-row
+                ,stream ,col-widths row 
+                (cdr (assoc 'vertical ,lookup-table))
+                :align ,align
+                :left-pad-str ,pad-str-var
+                :right-pad-str ,pad-str-var)
+               (format ,stream "~%")))
+         ,@body)
+       (truth-table/base::typeset-table-break
+        ,stream ,col-widths
+        (cdr (assoc 'horizontal ,lookup-table))
+        (cdr (assoc 'bottom-left ,lookup-table))
+        (cdr (assoc 'up ,lookup-table))
+        (cdr (assoc 'bottom-right ,lookup-table))
+        :right-pad-len ,padding
+        :left-pad-len ,padding))))
+
 (defun typeset-truth-table (table &optional
                                     (expr-lookup-table
                                      *operator-ascii-lookup-alist*)
@@ -355,47 +414,28 @@ between each row."
   (let* ((typeset-exprs (mapcar (lambda (expr)
                                   (typeset-proposition
                                    expr :lookup-table expr-lookup-table
-                                        :latin-truths latin-truths))
+                                   :latin-truths latin-truths))
                                 (extract-truth-table-expressions table)))
          (col-widths (mapcar (lambda (expr)
                                (+ (length expr) 2))
                              typeset-exprs)))
     (with-output-to-string (str)
-      (typeset-table-break str col-widths
-                           (cdr (assoc 'horizontal box-lookup-table))
-                           (cdr (assoc 'top-left box-lookup-table))
-                           (cdr (assoc 'down box-lookup-table))
-                           (cdr (assoc 'top-right box-lookup-table)))
-      (terpri str)
-      (typeset-table-row str col-widths typeset-exprs
-                         (cdr (assoc 'vertical box-lookup-table)))
-      (terpri str)
-      (typeset-table-break str col-widths
-                           (cdr (assoc 'horizontal box-lookup-table))
-                           (cdr (assoc 'right box-lookup-table))
-                           (cdr (assoc 'cross box-lookup-table))
-                           (cdr (assoc 'left box-lookup-table)))
-      (terpri str)
-      (dolist (row (extract-truth-table-values table))
-        (typeset-table-row str col-widths
-                           ;; convert t or nil to strings
-                           (mapcar (lambda (entry)
-                                     (cdr (assoc (if entry
-                                                     (if latin-truths
-                                                         'latin-true
-                                                         'true)
-                                                     (if latin-truths
-                                                         'latin-false
-                                                         'false))
-                                                 expr-lookup-table)))
-                                   row)
-                           (cdr (assoc 'vertical box-lookup-table)))
-        (terpri str))
-      (typeset-table-break str col-widths
-                           (cdr (assoc 'horizontal box-lookup-table))
-                           (cdr (assoc 'bottom-left box-lookup-table))
-                           (cdr (assoc 'up box-lookup-table))
-                           (cdr (assoc 'bottom-right box-lookup-table))))))
+      (with-draw-table (str col-widths box-lookup-table)
+        (:row typeset-exprs)
+        (:seperator)
+        (dolist (row (extract-truth-table-values table))
+          (:row (mapcar
+                 (lambda (entry)
+                   (cdr (assoc
+                         (if entry
+                             (if latin-truths
+                                 'latin-true
+                                 'true)
+                             (if latin-truths
+                                 'latin-false
+                                 'false))
+                         expr-lookup-table)))
+                 row)))))))
 
 (defparameter *known-formats*
   '("unicode" "ascii" "latex" "html")
diff --git a/web.lisp b/web.lisp
index b70cecf..dbf64ba 100644
--- a/web.lisp
+++ b/web.lisp
@@ -38,6 +38,94 @@
 (defparameter *default-address* "127.0.0.1")
 (defparameter *default-prefix* "/")
 
+(defwidget help-overlay ()
+  ()
+  (:documentation "Simple class to handle holding the help overlay."))
+
+(defmethod render ((overlay help-overlay))
+  (with-html
+    (:div :id "help-table-wrapper"
+     (:div :id "help-header-wrapper"
+      (:span :id "help-header" "Help")
+      (:span :id "help-close-button"
+       :onclick "document.querySelector(\".help-overlay\").style.display = \"none\""
+       "Close"))
+     (:table
+      (:tr (:th "Operator") (:th "Syntax"))
+      (loop for ((sym (name . nics) desc (examples)) . rest-desc)
+              = *operator-descriptions* then rest-desc
+            for ((_sym . syntax) . rest-st)
+              = *operator-symbol-table* then rest-st
+            while sym
+            do
+               (:tr
+                (:td name)
+                (:td (format nil "~{~a~^, ~}" (sort (copy-list syntax)
+                                                    'string<))))))
+     (:p "You can input multiple propositions by separating them with"
+      "commas (,):"
+      (:br)
+      (:code "ab,cd"))
+     (:p "Two operands next to each other is treated as an 'implicit and'"
+      "(unless this feature is disabled):"
+      (:br)
+      (:code (:raw "abc|d = a &and; b &and; c &or; d"))))))
+
+(defmethod get-dependencies ((overlay help-overlay))
+  (append
+   (list
+    (reblocks-lass:make-dependency
+      '(.help-overlay
+        :display "none"
+        :position "fixed"
+        :top "0px"
+        :left "0px"
+        :width "100%"
+        :height "100%"
+        :z-index "100" ;; be above EVERYTHING
+        (|#help-table-wrapper|
+         :background "#ffffff"
+         :border-width "2px"
+         :border-style "solid"
+         :border-color "black"
+         :padding "10px"
+         :width "fit-content"
+         :height "fit-content"
+         :position "fixed"
+         :top "40%"
+         :left "50%"
+         :transform translate "-50%" "-50%"
+         (|#help-header-wrapper|
+          :margin-bottom "3px"
+          :position "relative"
+          (|#help-header|
+           :font-size "x-large"
+           :font-weight "bold"
+           :display "block"
+           :text-align "center")
+          (|#help-close-button|
+           :user-select "none"
+           :text-decoration-line "underline"
+           :cursor "pointer"
+           :position "absolute"
+           :top "0"
+           :right "0"))
+         (table
+          :border-collapse "collapse"
+          :border-spacing "0px"
+          :margin "auto"
+          ((:or th td)
+           :padding "3px"
+           :padding-left "10px"
+           :padding-right "10px"
+           :text-align "left"
+           :border-style "solid"
+           :border-width "1px"
+           :border-color "black"))
+         (code
+          :padding-left "1em")))))
+   (call-next-method)))
+
 (defwidget truth-table ()
   ((data :initform nil
          :accessor truth-table-data)
@@ -77,24 +165,24 @@ reblocks bug.")
         (with-html
           (:div :class "label" "Output:")
           (:span :id "output-span"
-                 ;; there seems to be a bug in reblocks that means you have to pass
-                 ;; the second argument to `make-js-action'
-                 (:button :onclick (make-js-action
-                                    (lambda (&key &allow-other-keys)
-                                      (truth-table-toggle-output table)
-                                      (update table))
-                                    :args *blank-hash-table*)
-                          :id "output-expander-button"
-                          (if output-visible
-                              "⏷"
-                              "⏵"))
-                 (if (or pretty-print
-                         (equal format "ascii")
-                         (equal format "unicode"))
-                     (:pre :id "output-area" :hidden (not output-visible)
-                           other-text)
-                     (:code :id "output-area" :hidden (not output-visible)
-                            other-text)))
+           ;; there seems to be a bug in reblocks that means you have to pass
+           ;; the second argument to `make-js-action'
+           (:button :onclick (make-js-action
+                              (lambda (&key &allow-other-keys)
+                                (truth-table-toggle-output table)
+                                (update table))
+                              :args *blank-hash-table*)
+            :id "output-expander-button"
+            (if output-visible
+                "⏷"
+                "⏵"))
+           (if (or pretty-print
+                   (equal format "ascii")
+                   (equal format "unicode"))
+               (:pre :id "output-area" :hidden (not output-visible)
+                other-text)
+               (:code :id "output-area" :hidden (not output-visible)
+                other-text)))
           (:div :class "label" "HTML Preview:"))
         (princ html-text reblocks/html:*stream*))))
   nil)
@@ -175,9 +263,53 @@ reblocks bug.")
   ((table :initform (make-instance 'truth-table)
           :accessor page-table)
    (error-box :initform (make-instance 'error-box)
-              :accessor page-error-box))
+              :accessor page-error-box)
+   (help-overlay :initform (make-instance 'help-overlay)
+                 :accessor page-help-overlay))
   (:documentation "The root of the whole page"))
 
+(defun parse-and-eval-propositions (input-str &key implicit-and
+                                                multi-char-names
+                                                include-vars
+                                                include-intermediate)
+  "Parse and then eval all of comma separated props in INPUT-STR."
+  (let ((prop-start 0))
+    (handler-case
+        (loop
+          for prop-str in (uiop:split-string input-str :separator '(#\,))
+          for (parsed-exp vars) = (multiple-value-list
+                                   (parse-proposition-string
+                                    prop-str
+                                    :implicit-and implicit-and
+                                    :multi-char-names multi-char-names))
+          when parsed-exp
+            append vars into all-vars
+            and
+              collect parsed-exp into parsed-exps
+              and
+                do (incf prop-start (1+ (length prop-str)))
+          finally
+             (return (create-combined-truth-table
+                      parsed-exps
+                      (remove-duplicates all-vars :test 'equal
+                                                  :from-end t)
+                      :include-intermediate include-intermediate
+                      :include-vars include-vars)))
+      (proposition-parse-error (e)
+        ;; adjust the position and proposition string
+        (error 'proposition-parse-error
+               :message (parse-error-message e)
+               :proposition input-str
+               :position (+ (parse-error-position e)
+                            prop-start))))))
+
+(defun blank-prop-string-p (str)
+  "Return t if STR would produce a blank proposition table."
+  (not (find-if-not (lambda (c)
+                      (or (eq c #\,)
+                          (whitespace-p c)))
+                    str)))
+
 (defmethod handle-generate-request ((page page)
                                     &key prop-str implicit-and multi-char-names
                                       format include-vars subexps latin pretty)
@@ -185,19 +317,17 @@ reblocks bug.")
   (with-slots (table error-box) page
     (setf (truth-table-format table) format
           (error-box-message error-box) nil)
-    (if (not (zerop (length prop-str)))
+    (if (not (blank-prop-string-p prop-str))
         (handler-case
-            (multiple-value-bind (parsed-exp vars)
-                (parse-proposition-string
-                 prop-str
-                 :implicit-and implicit-and
-                 :multi-char-names multi-char-names)
-              (setf (truth-table-data table) (create-truth-table parsed-exp
-                                              :vars vars
-                                              :include-vars include-vars
-                                              :include-intermediate subexps)
-                    (truth-table-latin-truths table) latin
-                    (truth-table-pretty-print table) pretty))
+            (setf (truth-table-data table)
+                  (parse-and-eval-propositions
+                   prop-str
+                   :implicit-and implicit-and
+                   :multi-char-names multi-char-names
+                   :include-vars include-vars
+                   :include-intermediate subexps)
+                  (truth-table-latin-truths table) latin
+                  (truth-table-pretty-print table) pretty)
           ((or proposition-parse-error proposition-eval-error) (e)
             (setf (error-box-message error-box) (princ-to-string e))))
         (setf (truth-table-data table) nil))
@@ -207,76 +337,86 @@ reblocks bug.")
 (defmethod render ((page page))
   "Render PAGE."
   (with-html
-    (with-slots (table error-box) page
-      (:h1 "Truth Table Generator")
-      (with-html-form (:POST (lambda (&key prop-str implicit-and
-                                        multi-char-names format
-                                        include-vars subexps latin
-                                        pretty
-                                      &allow-other-keys)
-                               (handle-generate-request
-                                page :prop-str prop-str
-                                     :implicit-and implicit-and
-                                     :multi-char-names multi-char-names
-                                     :format format
-                                     :include-vars include-vars
-                                     :subexps subexps
-                                     :pretty pretty
-                                     :latin latin)))
-        (:div :id "main-controls-wrapper"
-              (:input :id "prop-input-field"
-                      :type "text"
-                      :name "prop-str"
-                      :placeholder "Proposition string...")
-              (:input :id "submit-button"
-                      :type "submit"
-                      :value "Generate"))
-        (:div :id "extra-controls-wrapper"
-              (:input :type "checkbox"
-                      :name "implicit-and"
-                      :checked t)
-              (:label :for "implicit-and" "Implicit And")
-              (:input :type "checkbox"
-                      :name "multi-char-names"
-                      :style "margin-left: 10px;")
-              (:label :for "multi-char-names" "Multi-character Variables")
-              (:input :type "checkbox"
-                      :name "include-vars"
-                      :checked t
-                      :style "margin-left: 10px;")
-              (:label :for "include-vars" "Include Variables")
-              (:input :type "checkbox"
-                      :name "subexps"
-                      :checked t
-                      :style "margin-left: 10px;")
-              (:label :for "subexps" "Include Sub-expressions")
-              (:input :type "checkbox"
-                      :name "pretty"
-                      :checked t
-                      :style "margin-left: 10px;")
-              (:label :for "pretty" "Pretty Print")
-              (:input :type "checkbox"
-                      :name "latin"
-                      :checked nil
-                      :style "margin-left: 10px;")
-              (:label :for "latin" "Latin Truth Values")
-              (:select :name "format" :style "margin-left: 10px;"
-                (:option :value "html" "HTML")
-                (:option :value "latex" "LaTeX")
-                (:option :value "ascii" "ASCII")
-                (:option :value "unicode" "Unicode"))))
-      (render error-box)
-      (render table)
-      (:div :id "info-text"
-            (:span 
-             "This website is free software under the terms of the AGPL"
-             "license version 3. You can find a copy of the license ")
-            (:a :href "https://www.gnu.org/licenses/agpl-3.0.html"
-                "here")
-            (:span ". You can find the source of this website ")
-            (:a :href "https://git.zander.im/Zander671/truth-table"
-                "here")
-            (:span ".")))))
+    (:doctype)
+    (:html
+     (:head
+      (:title "Truth Table Generator"))
+     (:body
+      (with-slots (table error-box help-overlay) page
+        (render help-overlay)
+        (:h1 "Truth Table Generator")
+        (with-html-form (:POST (lambda (&key prop-str implicit-and
+                                          multi-char-names format
+                                          include-vars subexps latin
+                                          pretty
+                                        &allow-other-keys)
+                                 (handle-generate-request
+                                  page :prop-str prop-str
+                                  :implicit-and implicit-and
+                                  :multi-char-names multi-char-names
+                                  :format format
+                                  :include-vars include-vars
+                                  :subexps subexps
+                                  :pretty pretty
+                                  :latin latin)))
+          (:div :id "main-controls-wrapper"
+           (:input :id "prop-input-field"
+            :type "text"
+            :name "prop-str"
+            :placeholder "Proposition string...")
+           (:input :id "submit-button"
+            :type "submit"
+            :value "Generate")
+           (:button :id "help-button"
+            :onclick
+            "document.querySelector(\".help-overlay\").style.display = \"initial\""
+            "Help"))
+          (:div :id "extra-controls-wrapper"
+           (:input :type "checkbox"
+            :name "implicit-and"
+            :checked t)
+           (:label :for "implicit-and" "Implicit And")
+           (:input :type "checkbox"
+            :name "multi-char-names"
+            :style "margin-left: 10px;")
+           (:label :for "multi-char-names" "Multi-character Variables")
+           (:input :type "checkbox"
+            :name "include-vars"
+            :checked t
+            :style "margin-left: 10px;")
+           (:label :for "include-vars" "Include Variables")
+           (:input :type "checkbox"
+            :name "subexps"
+            :checked t
+            :style "margin-left: 10px;")
+           (:label :for "subexps" "Include Sub-expressions")
+           (:input :type "checkbox"
+            :name "pretty"
+            :checked t
+            :style "margin-left: 10px;")
+           (:label :for "pretty" "Pretty Print")
+           (:input :type "checkbox"
+            :name "latin"
+            :checked nil
+            :style "margin-left: 10px;")
+           (:label :for "latin" "Latin Truth Values")
+           (:select :name "format" :style "margin-left: 10px;"
+            (:option :value "html" "HTML")
+            (:option :value "latex" "LaTeX")
+            (:option :value "ascii" "ASCII")
+            (:option :value "unicode" "Unicode"))))
+        (render error-box)
+        (render table)
+        (:div :id "info-text"
+         (:span 
+          "This website is free software under the terms of the AGPL"
+          "license version 3. You can find a copy of the license ")
+         (:a :href "https://www.gnu.org/licenses/agpl-3.0.html"
+          "here")
+         (:span ". You can find the source of this website ")
+         (:a :href "https://git.zander.im/Zander671/truth-table"
+          "here")
+         (:span ".")))))))
 
 (defmethod get-dependencies ((page page))
   (append
@@ -290,13 +430,15 @@ reblocks bug.")
          :margin-bottom "5px"
          (|#main-controls-wrapper|
           :display flex
-           :margin-bottom "5px"
+          :margin-bottom "5px"
           (|#prop-input-field|
            :flex-grow "1"
            :margin-right "5px"
            :font-size "large")
-          (|#submit-button|
-           :font-size "large"))
+          ((:or |#submit-button| |#help-button|)
+           :font-size "large")
+          (|#help-button|
+           :margin-left "5px"))
          (|#extra-controls-wrapper|
           :display "flex"
           :justify-content "center"