# HG changeset patch
# User wenzelm
# Date 1533558586 -7200
# Node ID 29dbf3408021ed1b33cfb2c1fd804995479a6b52
# Parent  2862b585a0db3b2b797e67bfa9200c3c0b2646db
updated documentation;

diff -r 2862b585a0db -r 29dbf3408021 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Aug 02 16:02:56 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Aug 06 14:29:46 2018 +0200
@@ -365,9 +365,9 @@
 text \<open>
   In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
-  pixels as adequate for text rendering. In 2017, we routinely see much higher
-  resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
-  ``4K'' at $3840 \times 2160$.
+  pixels as adequate for text rendering. After 2016, we have routinely seen
+  much higher resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or
+  ``Ultra HD'' / ``4K'' at $3840 \times 2160$.
 
   GUI frameworks are usually lagging behind, with hard-wired icon sizes and
   tiny fonts. Java and jEdit do provide reasonable support for very high
@@ -1381,14 +1381,20 @@
 
   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).
+  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require additional
+  interaction to confirm (via popup). This 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.
 
-  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.
+  Special symbols like \<^verbatim>\<open>\<comment>\<close> or control symbols like \<^verbatim>\<open>\<^cancel>\<close>,
+  \<^verbatim>\<open>\<^latex>\<close>, \<^verbatim>\<open>\<^binding>\<close> can have an argument: completing on a name
+  prefix offers a template with an empty cartouche. Thus completion of \<^verbatim>\<open>\co\<close>
+  or \<^verbatim>\<open>\ca\<close> allows to compose formal document comments quickly.\<^footnote>\<open>It is
+  customary to put a space between \<^verbatim>\<open>\<comment>\<close> and its argument, while
+  control symbols do \<^emph>\<open>not\<close> allow extra space here.\<close>
 \<close>
 
 
@@ -1889,11 +1895,13 @@
   \label{fig:cite-completion}
   \end{figure}
 
-  Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files
+  Isabelle/jEdit also provides IDE support for editing \<^verbatim>\<open>.bib\<close> files
   themselves. There is syntax highlighting based on entry types (according to
   standard Bib{\TeX} styles), a context-menu to compose entries
   systematically, and a SideKick tree view of the overall content; see
-  \figref{fig:bibtex-mode}.
+  \figref{fig:bibtex-mode}. Semantic checking with errors and warnings is
+  performed by the original \<^verbatim>\<open>bibtex\<close> tool using style \<^verbatim>\<open>plain\<close>: different
+  Bib{\TeX} styles may produce slightly different results.
 
   \begin{figure}[!htb]
   \begin{center}
@@ -1902,10 +1910,14 @@
   \caption{Bib{\TeX} mode with context menu and SideKick tree view}
   \label{fig:bibtex-mode}
   \end{figure}
+
+  Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
+  approximates the usual {\LaTeX} bibliography output in HTML (using style
+  \<^verbatim>\<open>unsort\<close>).
 \<close>
 
 
-section \<open>Document preview\<close>
+section \<open>Document preview \label{sec:document-preview}\<close>
 
 text \<open>
   The action @{action_def isabelle.preview} opens an HTML preview of the