# HG changeset patch
# User wenzelm
# Date 1479665294 -3600
# Node ID 56972c75502766f7b8c9b4dca6425f7e719b5225
# Parent  2b90410090ee134ebf046670d0b6d0bcadcd6c2c
misc tuning and updates;

diff -r 2b90410090ee -r 56972c755027 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 17:10:30 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 19:08:14 2016 +0100
@@ -141,8 +141,7 @@
   done with the usual care for such an open bazaar of contributions. Arbitrary
   combinations of add-on features are apt to cause problems. It is advisable
   to start with the default configuration of Isabelle/jEdit and develop some
-  understanding how it is supposed to work, before loading too many other
-  plugins.
+  sense how it is meant to work, before loading too many other plugins.
 
   \<^medskip>
   The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
@@ -207,12 +206,15 @@
   first start of the editor; afterwards the keymap file takes precedence and
   is no longer affected by change of default properties.
 
-  This subtle difference of jEdit keymaps versus properties is relevant for
-  Isabelle/jEdit due to various fine-tuning of global defaults, with
-  additional keyboard shortcuts for Isabelle-specific functionality. Users may
-  change their keymap later, but need to copy some keyboard shortcuts manually
-  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
-  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
+  Users may change their keymap later, but need to keep its content @{path
+  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
+  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
+
+  \<^medskip>
+  The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
+  Isabelle keymap changes that are in conflict with the current jEdit keymap;
+  non-conflicting changes are always applied implicitly. This action is
+  automatically invoked on Isabelle/jEdit startup.
 \<close>
 
 
@@ -292,7 +294,7 @@
 
   The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   different server name. The default server name is the official distribution
-  name (e.g.\ \<^verbatim>\<open>Isabelle2016\<close>). Thus @{tool jedit_client} can connect to the
+  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
   Isabelle desktop application without further options.
 
   The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
@@ -699,9 +701,9 @@
 text \<open>
   The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
   structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
-  main mode for theory files, as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file
-  (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system \<^verbatim>\<open>options\<close>, and
-  Bib{\TeX} files (\secref{sec:bibtex}).
+  main mode for theory files, ML files, as well as some minor modes for the
+  \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
+  \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
 
   \begin{figure}[!htb]
   \begin{center}
@@ -711,6 +713,19 @@
   \label{fig:sidekick}
   \end{figure}
 
+  The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
+  tree-view on the formal document structure, with section headings at the top
+  and formal specification elements at the bottom. The alternative parser
+  \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
+  end\<close> structure.
+
+  \<^medskip>
+  Isabelle/ML files are structured according to semi-formal comments that are
+  explained in @{cite "isabelle-implementation"}. This outline is turned into
+  a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
+  folding mode of the same name, for hierarchic text folds within ML files.
+
+  \<^medskip>
   The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
   markup tree of the PIDE document model of the current buffer. This is
   occasionally useful for informative purposes, but the amount of displayed
@@ -1199,12 +1214,12 @@
   kinds and purposes. The completion mechanism supports this by the following
   built-in templates:
 
-    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close> via text
-    cartouches. There are three selections, which are always presented in the
-    same order and do not depend on any context information. The default
-    choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the cursor
-    position after insertion; the other choices help to repair the block
-    structure of unbalanced text cartouches.
+    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
+    \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are
+    always presented in the same order and do not depend on any context
+    information. The default choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the
+    box indicates the cursor position after insertion; the other choices help
+    to repair the block structure of unbalanced text cartouches.
 
     \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
     the cursor position after insertion. Here it is convenient to use the
@@ -1213,8 +1228,8 @@
 
   With some practice, input of quoted sub-languages and antiquotations of
   embedded languages should work fluently. Note that national keyboard layouts
-  might cause problems with back-quote as dead key: if possible, dead keys
-  should be disabled.
+  might cause problems with back-quote as dead key, but double quote can be
+  used instead.
 \<close>
 
 
@@ -1274,6 +1289,20 @@
 \<close>
 
 
+subsubsection \<open>User-defined abbreviations\<close>
+
+text \<open>
+  The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
+  @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
+  templates and abbreviations for Isabelle symbols, as explained above.
+  Examples may be found in the Isabelle sources, by searching for
+  ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
+
+  The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
+  current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
+\<close>
+
+
 subsubsection \<open>Name-space entries\<close>
 
 text \<open>