src/Doc/JEdit/JEdit.thy
changeset 64513 56972c755027
parent 64512 2b90410090ee
child 64514 27914a4f8c70
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 17:10:30 2016 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 19:08:14 2016 +0100
     1.3 @@ -141,8 +141,7 @@
     1.4    done with the usual care for such an open bazaar of contributions. Arbitrary
     1.5    combinations of add-on features are apt to cause problems. It is advisable
     1.6    to start with the default configuration of Isabelle/jEdit and develop some
     1.7 -  understanding how it is supposed to work, before loading too many other
     1.8 -  plugins.
     1.9 +  sense how it is meant to work, before loading too many other plugins.
    1.10  
    1.11    \<^medskip>
    1.12    The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
    1.13 @@ -207,12 +206,15 @@
    1.14    first start of the editor; afterwards the keymap file takes precedence and
    1.15    is no longer affected by change of default properties.
    1.16  
    1.17 -  This subtle difference of jEdit keymaps versus properties is relevant for
    1.18 -  Isabelle/jEdit due to various fine-tuning of global defaults, with
    1.19 -  additional keyboard shortcuts for Isabelle-specific functionality. Users may
    1.20 -  change their keymap later, but need to copy some keyboard shortcuts manually
    1.21 -  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
    1.22 -  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
    1.23 +  Users may change their keymap later, but need to keep its content @{path
    1.24 +  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
    1.25 +  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
    1.26 +
    1.27 +  \<^medskip>
    1.28 +  The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
    1.29 +  Isabelle keymap changes that are in conflict with the current jEdit keymap;
    1.30 +  non-conflicting changes are always applied implicitly. This action is
    1.31 +  automatically invoked on Isabelle/jEdit startup.
    1.32  \<close>
    1.33  
    1.34  
    1.35 @@ -292,7 +294,7 @@
    1.36  
    1.37    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
    1.38    different server name. The default server name is the official distribution
    1.39 -  name (e.g.\ \<^verbatim>\<open>Isabelle2016\<close>). Thus @{tool jedit_client} can connect to the
    1.40 +  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
    1.41    Isabelle desktop application without further options.
    1.42  
    1.43    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
    1.44 @@ -699,9 +701,9 @@
    1.45  text \<open>
    1.46    The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
    1.47    structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
    1.48 -  main mode for theory files, as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file
    1.49 -  (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system \<^verbatim>\<open>options\<close>, and
    1.50 -  Bib{\TeX} files (\secref{sec:bibtex}).
    1.51 +  main mode for theory files, ML files, as well as some minor modes for the
    1.52 +  \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
    1.53 +  \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
    1.54  
    1.55    \begin{figure}[!htb]
    1.56    \begin{center}
    1.57 @@ -711,6 +713,19 @@
    1.58    \label{fig:sidekick}
    1.59    \end{figure}
    1.60  
    1.61 +  The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
    1.62 +  tree-view on the formal document structure, with section headings at the top
    1.63 +  and formal specification elements at the bottom. The alternative parser
    1.64 +  \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
    1.65 +  end\<close> structure.
    1.66 +
    1.67 +  \<^medskip>
    1.68 +  Isabelle/ML files are structured according to semi-formal comments that are
    1.69 +  explained in @{cite "isabelle-implementation"}. This outline is turned into
    1.70 +  a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
    1.71 +  folding mode of the same name, for hierarchic text folds within ML files.
    1.72 +
    1.73 +  \<^medskip>
    1.74    The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
    1.75    markup tree of the PIDE document model of the current buffer. This is
    1.76    occasionally useful for informative purposes, but the amount of displayed
    1.77 @@ -1199,12 +1214,12 @@
    1.78    kinds and purposes. The completion mechanism supports this by the following
    1.79    built-in templates:
    1.80  
    1.81 -    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close> via text
    1.82 -    cartouches. There are three selections, which are always presented in the
    1.83 -    same order and do not depend on any context information. The default
    1.84 -    choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the cursor
    1.85 -    position after insertion; the other choices help to repair the block
    1.86 -    structure of unbalanced text cartouches.
    1.87 +    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
    1.88 +    \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are
    1.89 +    always presented in the same order and do not depend on any context
    1.90 +    information. The default choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the
    1.91 +    box indicates the cursor position after insertion; the other choices help
    1.92 +    to repair the block structure of unbalanced text cartouches.
    1.93  
    1.94      \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
    1.95      the cursor position after insertion. Here it is convenient to use the
    1.96 @@ -1213,8 +1228,8 @@
    1.97  
    1.98    With some practice, input of quoted sub-languages and antiquotations of
    1.99    embedded languages should work fluently. Note that national keyboard layouts
   1.100 -  might cause problems with back-quote as dead key: if possible, dead keys
   1.101 -  should be disabled.
   1.102 +  might cause problems with back-quote as dead key, but double quote can be
   1.103 +  used instead.
   1.104  \<close>
   1.105  
   1.106  
   1.107 @@ -1274,6 +1289,20 @@
   1.108  \<close>
   1.109  
   1.110  
   1.111 +subsubsection \<open>User-defined abbreviations\<close>
   1.112 +
   1.113 +text \<open>
   1.114 +  The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
   1.115 +  @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
   1.116 +  templates and abbreviations for Isabelle symbols, as explained above.
   1.117 +  Examples may be found in the Isabelle sources, by searching for
   1.118 +  ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
   1.119 +
   1.120 +  The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
   1.121 +  current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
   1.122 +\<close>
   1.123 +
   1.124 +
   1.125  subsubsection \<open>Name-space entries\<close>
   1.126  
   1.127  text \<open>