updated documentation;
authorwenzelm
Mon Aug 06 14:29:46 2018 +0200 (11 days ago)
changeset 6873629dbf3408021
parent 68735 2862b585a0db
child 68737 a8bef9ff7dc0
updated documentation;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Aug 02 16:02:56 2018 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Aug 06 14:29:46 2018 +0200
     1.3 @@ -365,9 +365,9 @@
     1.4  text \<open>
     1.5    In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
     1.6    pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
     1.7 -  pixels as adequate for text rendering. In 2017, we routinely see much higher
     1.8 -  resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
     1.9 -  ``4K'' at $3840 \times 2160$.
    1.10 +  pixels as adequate for text rendering. After 2016, we have routinely seen
    1.11 +  much higher resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or
    1.12 +  ``Ultra HD'' / ``4K'' at $3840 \times 2160$.
    1.13  
    1.14    GUI frameworks are usually lagging behind, with hard-wired icon sizes and
    1.15    tiny fonts. Java and jEdit do provide reasonable support for very high
    1.16 @@ -1381,14 +1381,20 @@
    1.17  
    1.18    Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
    1.19    language context (\secref{sec:completion-context}). In contrast, backslash
    1.20 -  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require
    1.21 -  additional interaction to confirm (via popup).
    1.22 +  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require additional
    1.23 +  interaction to confirm (via popup). This is important in ambiguous
    1.24 +  situations, e.g.\ for Isabelle document source, which may contain formal
    1.25 +  symbols or informal {\LaTeX} macros. Backslash sequences also help when
    1.26 +  input is broken, and thus escapes its normal semantic context: e.g.\
    1.27 +  antiquotations or string literals in ML, which do not allow arbitrary
    1.28 +  backslash sequences.
    1.29  
    1.30 -  The latter is important in ambiguous situations, e.g.\ for Isabelle document
    1.31 -  source, which may contain formal symbols or informal {\LaTeX} macros.
    1.32 -  Backslash sequences also help when input is broken, and thus escapes its
    1.33 -  normal semantic context: e.g.\ antiquotations or string literals in ML,
    1.34 -  which do not allow arbitrary backslash sequences.
    1.35 +  Special symbols like \<^verbatim>\<open>\<comment>\<close> or control symbols like \<^verbatim>\<open>\<^cancel>\<close>,
    1.36 +  \<^verbatim>\<open>\<^latex>\<close>, \<^verbatim>\<open>\<^binding>\<close> can have an argument: completing on a name
    1.37 +  prefix offers a template with an empty cartouche. Thus completion of \<^verbatim>\<open>\co\<close>
    1.38 +  or \<^verbatim>\<open>\ca\<close> allows to compose formal document comments quickly.\<^footnote>\<open>It is
    1.39 +  customary to put a space between \<^verbatim>\<open>\<comment>\<close> and its argument, while
    1.40 +  control symbols do \<^emph>\<open>not\<close> allow extra space here.\<close>
    1.41  \<close>
    1.42  
    1.43  
    1.44 @@ -1889,11 +1895,13 @@
    1.45    \label{fig:cite-completion}
    1.46    \end{figure}
    1.47  
    1.48 -  Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files
    1.49 +  Isabelle/jEdit also provides IDE support for editing \<^verbatim>\<open>.bib\<close> files
    1.50    themselves. There is syntax highlighting based on entry types (according to
    1.51    standard Bib{\TeX} styles), a context-menu to compose entries
    1.52    systematically, and a SideKick tree view of the overall content; see
    1.53 -  \figref{fig:bibtex-mode}.
    1.54 +  \figref{fig:bibtex-mode}. Semantic checking with errors and warnings is
    1.55 +  performed by the original \<^verbatim>\<open>bibtex\<close> tool using style \<^verbatim>\<open>plain\<close>: different
    1.56 +  Bib{\TeX} styles may produce slightly different results.
    1.57  
    1.58    \begin{figure}[!htb]
    1.59    \begin{center}
    1.60 @@ -1902,10 +1910,14 @@
    1.61    \caption{Bib{\TeX} mode with context menu and SideKick tree view}
    1.62    \label{fig:bibtex-mode}
    1.63    \end{figure}
    1.64 +
    1.65 +  Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
    1.66 +  approximates the usual {\LaTeX} bibliography output in HTML (using style
    1.67 +  \<^verbatim>\<open>unsort\<close>).
    1.68  \<close>
    1.69  
    1.70  
    1.71 -section \<open>Document preview\<close>
    1.72 +section \<open>Document preview \label{sec:document-preview}\<close>
    1.73  
    1.74  text \<open>
    1.75    The action @{action_def isabelle.preview} opens an HTML preview of the