more on "Completion";

--- a/src/Doc/JEdit/JEdit.thy	Fri Jun 13 21:58:12 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 13 22:15:13 2014 +0200
@@ -1041,12 +1041,33 @@
 
 subsection {* Varieties of completion \label{sec:completion-varieties} *}
 
-text {* FIXME *}
+subsubsection {* Built-in templates *}
 
+text {*
+  Isabelle is ultimately a framework of nested sub-languages of different
+  kinds and purposes.  The completion mechanism supports this by two built-in
+  templates:
+  \begin{enumerate}
 
-subsubsection {* Templates *}
+  \item @{verbatim "`"} (single ASCII back-quote) supports \emph{quotations}
+  via text cartouches. There are three selections, which are always presented
+  in this order and do not depend on any context information. The default
+  choice produces a template ``@{text "\<open>\<box>\<close>"}'', where the box indicates the
+  cursor position after insertion; the other choices help to repair the block
+  structure of unbalanced text cartouches.
 
-text {* FIXME *}
+  \item @{verbatim "@{"} is completed to the template ``@{text "@{\<box>}"}'' where
+  the box indicates the cursor position after insertion. Here it is convenient
+  to use ``@{verbatim __}'' or more specific name prefixes to let semantic
+  completion of name-space entries propose antiquotation names.
+
+  \end{enumerate}
+
+  With some practice, the nesting of quoted sub-languages and antiquotations
+  with other languages should work fluently. Note that national keyboard
+  layouts might cause problems with back-quote as dead key: if possible, dead
+  keys are better disabled.
+*}
 
 
 subsubsection {* Symbols *}

--- a/src/Doc/JEdit/document/root.tex	Fri Jun 13 21:58:12 2014 +0200
+++ b/src/Doc/JEdit/document/root.tex	Fri Jun 13 22:15:13 2014 +0200
@@ -4,6 +4,7 @@
 \usepackage{graphicx}
 \usepackage{iman,extra,isar,ttbox}
 \usepackage[nohyphen,strings]{underscore}
+\usepackage{amssymb}
 \usepackage{isabelle,isabellesym}
 \usepackage{railsetup}
 \usepackage{style}