# HG changeset patch
# User wenzelm
# Date 1503255183 -7200
# Node ID 0a8277e9cfd6e77d326eb141c4985213579992b6
# Parent  0b55fbc51f76870c4d5b2493162dc7bfe3273dc5
officially allow restart of Isabelle plugin;

diff -r 0b55fbc51f76 -r 0a8277e9cfd6 NEWS
--- a/NEWS	Sun Aug 20 20:38:37 2017 +0200
+++ b/NEWS	Sun Aug 20 20:53:03 2017 +0200
@@ -105,6 +105,10 @@
 painted with thick lines; remaining errors in this situation are
 represented by a different border color.
 
+* The main Isabelle/jEdit plugin may be restarted manually (using the
+jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
+enabled at all times.
+
 * Update to jedit-5.4.0.
 
 
diff -r 0b55fbc51f76 -r 0a8277e9cfd6 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Aug 20 20:38:37 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sun Aug 20 20:53:03 2017 +0200
@@ -144,17 +144,16 @@
   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
-  to remain active at all times! A few additional plugins are bundled with
-  Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with
-  its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>
-  with some Isabelle-specific parsers for document tree structure
-  (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important
-  for hyperlinks within the formal document-model
-  (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,
-  \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,
-  but have no particular use in Isabelle/jEdit.
-\<close>
+  The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
+  Isabelle/jEdit: it manages the prover session in the background. A few
+  additional plugins are bundled with Isabelle/jEdit for convenience or out of
+  necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
+  (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
+  parsers for document tree structure (\secref{sec:sidekick}). The
+  \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
+  formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
+  (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
+  of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
 
 
 subsection \<open>Options \label{sec:options}\<close>
@@ -497,13 +496,14 @@
 paragraph \<open>Encoding.\<close>
 text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
   \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
-  JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for
-  all source files. Sometimes such defaults are reset accidentally, or
-  malformed UTF-8 sequences in the text force jEdit to fall back on a
-  different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will
-  be shown in the text buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The
-  jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps
-  to resolve such problems (after repairing malformed parts of the text). \<close>
+  JVM). It is provided by the Isabelle Base plugin and enabled by default for
+  all source files in Isabelle/jEdit. Sometimes such defaults are reset
+  accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
+  back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim
+  ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its Unicode rendering
+  ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/
+  UTF-8-Isabelle\<close> helps to resolve such problems (after repairing malformed
+  parts of the text). \<close>
 
 paragraph \<open>Font.\<close>
 text \<open>Correct rendering via Unicode requires a font that contains glyphs for