src/Doc/JEdit/JEdit.thy

 
   A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a
   syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more
   aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
 
+  Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
+  language context (\secref{sec:completion-context}). In contrast, backslash
+  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require
+  additional interaction to confirm (via popup).
+
+  The latter is important in ambiguous situations, e.g.\ for Isabelle document
+  source, which may contain formal symbols or informal {\LaTeX} macros.
+  Backslash sequences also help when input is broken, and thus escapes its
+  normal semantic context: e.g.\ antiquotations or string literals in ML,
+  which do not allow arbitrary backslash sequences.
+
   \<^medskip>
   Additional abbreviations may be specified in @{file
   "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
   "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
   outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
   ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
   than just one symbol; otherwise the meaning is the same as a symbol
   specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
   "etc/symbols"}.
-
-  \<^medskip>
-  Symbol completion depends on the semantic language context
-  (\secref{sec:completion-context}), to enable or disable that aspect for a
-  particular sub-language of Isabelle. For example, symbol completion is
-  suppressed within document source to avoid confusion with {\LaTeX} macros
-  that use similar notation.
 \<close>
 
 
 subsubsection \<open>Name-space entries\<close>
 

 
 
 subsubsection \<open>File-system paths\<close>
 
 text \<open>
-  Depending on prover markup about file-system path specifications in the
-  source text, e.g.\ for the argument of a load command
-  (\secref{sec:aux-files}), the completion mechanism explores the directory
-  content and offers the result as completion popup. Relative path
-  specifications are understood wrt.\ the \<^emph>\<open>master directory\<close> of the document
-  node (\secref{sec:buffer-node}) of the enclosing editor buffer; this
-  requires a proper theory, not an auxiliary file.
+  Depending on prover markup about file-system paths in the source text, e.g.\
+  for the argument of a load command (\secref{sec:aux-files}), the completion
+  mechanism explores the directory content and offers the result as completion
+  popup. Relative path specifications are understood wrt.\ the \<^emph>\<open>master
+  directory\<close> of the document node (\secref{sec:buffer-node}) of the enclosing
+  editor buffer; this requires a proper theory, not an auxiliary file.
 
   A suffix of slashes may be used to continue the exploration of an already
   recognized directory name.
 \<close>
 

   default keyboard shortcut \<^verbatim>\<open>C+b\<close>.
 
   \<^medskip>
   Dictionary lookup uses some educated guesses about lower-case, upper-case,
   and capitalized words. This is oriented on common use in English, where this
-  aspect is not decisive for proper spelling, in contrast to German, for
-  example.
+  aspect is not decisive for proper spelling (in contrast to German, for
+  example).
 \<close>
 
 
 subsection \<open>Semantic completion context \label{sec:completion-context}\<close>
 

   is required. Until that information becomes available in the PIDE
   document-model, the default context is given by the outer syntax of the
   editor mode (see also \secref{sec:buffer-node}).
 
   The semantic \<^emph>\<open>language context\<close> provides information about nested
-  sub-languages of Isabelle: keywords are only completed for outer syntax,
-  symbols or antiquotations for languages that support them. E.g.\ there is no
-  symbol completion for ML source, but within ML strings, comments,
-  antiquotations.
+  sub-languages of Isabelle: keywords are only completed for outer syntax, and
+  antiquotations for languages that support them. Symbol abbreviations only
+  work for specific sub-languages: e.g.\ ``\<^verbatim>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in
+  regular ML source, but is completed within ML strings, comments,
+  antiquotations. Backslash representations of symbols like ``\<^verbatim>\<open>\foobar\<close>'' or
+  ``\<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.
 
   The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to
   tell that some language keywords should be excluded from further completion
-  attempts. For example, \<^verbatim>\<open>:\<close> within accepted Isar syntax looses its meaning
-  as abbreviation for symbol \<open>\<in>\<close>.
-
-  \<^medskip>
-  The completion context is \<^emph>\<open>ignored\<close> for built-in templates and symbols in
-  their explicit form ``\<^verbatim>\<open>\<foobar>\<close>''; see also
-  \secref{sec:completion-varieties}. This allows to complete within broken
-  input that escapes its normal semantic context, e.g.\ antiquotations or
-  string literals in ML, which do not allow arbitrary backslash sequences.
+  attempts. For example, ``\<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its
+  meaning as abbreviation for symbol ``\<open>\<in>\<close>''.
 \<close>
 
 
 subsection \<open>Input events \label{sec:completion-input}\<close>
 

 
     \<^enum> The system option @{system_option_ref jedit_completion_immediate}
     (enabled by default) controls whether replacement text should be inserted
     immediately without popup, regardless of @{system_option
     jedit_completion_delay}. This aggressive mode of completion is restricted
-    to Isabelle symbols and their abbreviations (\secref{sec:symbols}).
+    to symbol abbreviations that are not plain words (\secref{sec:symbols}).
 
     \<^enum> Completion of symbol abbreviations with only one relevant character in
     the text always enforces an explicit popup, regardless of
     @{system_option_ref jedit_completion_immediate}.
 \<close>

   frequency of selection, with persistent history. The popup may interpret
   special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>,
   \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text
   area. This allows to ignore unwanted completions most of the time and
   continue typing quickly. Thus the popup serves as a mechanism of
-  confirmation of proposed items, but the default is to continue without
+  confirmation of proposed items, while the default is to continue without
   completion.
 
   The meaning of special keys is as follows:
 
   \<^medskip>

   jedit_completion_immediate} determine the handling of keyboard events for
   implicit completion (\secref{sec:completion-input}).
 
   A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of
   key events, until after the user has stopped typing for the given time span,
-  but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close> means that
+  but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that
   abbreviations of Isabelle symbols are handled nonetheless.
 
   \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
   patterns to ignore in file-system path completion (separated by colons),
   e.g.\ backup files ending with tilde.