officially allow restart of Isabelle plugin;
authorwenzelm
Sun Aug 20 20:53:03 2017 +0200 (21 months ago)
changeset 664620a8277e9cfd6
parent 66461 0b55fbc51f76
child 66463 934bd55d768a
officially allow restart of Isabelle plugin;
NEWS
src/Doc/JEdit/JEdit.thy
     1.1 --- a/NEWS	Sun Aug 20 20:38:37 2017 +0200
     1.2 +++ b/NEWS	Sun Aug 20 20:53:03 2017 +0200
     1.3 @@ -105,6 +105,10 @@
     1.4  painted with thick lines; remaining errors in this situation are
     1.5  represented by a different border color.
     1.6  
     1.7 +* The main Isabelle/jEdit plugin may be restarted manually (using the
     1.8 +jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
     1.9 +enabled at all times.
    1.10 +
    1.11  * Update to jedit-5.4.0.
    1.12  
    1.13  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Aug 20 20:38:37 2017 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Aug 20 20:53:03 2017 +0200
     2.3 @@ -144,17 +144,16 @@
     2.4    sense how it is meant to work, before loading too many other plugins.
     2.5  
     2.6    \<^medskip>
     2.7 -  The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
     2.8 -  to remain active at all times! A few additional plugins are bundled with
     2.9 -  Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with
    2.10 -  its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>
    2.11 -  with some Isabelle-specific parsers for document tree structure
    2.12 -  (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important
    2.13 -  for hyperlinks within the formal document-model
    2.14 -  (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,
    2.15 -  \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,
    2.16 -  but have no particular use in Isabelle/jEdit.
    2.17 -\<close>
    2.18 +  The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
    2.19 +  Isabelle/jEdit: it manages the prover session in the background. A few
    2.20 +  additional plugins are bundled with Isabelle/jEdit for convenience or out of
    2.21 +  necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
    2.22 +  (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
    2.23 +  parsers for document tree structure (\secref{sec:sidekick}). The
    2.24 +  \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
    2.25 +  formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
    2.26 +  (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
    2.27 +  of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
    2.28  
    2.29  
    2.30  subsection \<open>Options \label{sec:options}\<close>
    2.31 @@ -497,13 +496,14 @@
    2.32  paragraph \<open>Encoding.\<close>
    2.33  text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
    2.34    \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
    2.35 -  JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for
    2.36 -  all source files. Sometimes such defaults are reset accidentally, or
    2.37 -  malformed UTF-8 sequences in the text force jEdit to fall back on a
    2.38 -  different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will
    2.39 -  be shown in the text buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The
    2.40 -  jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps
    2.41 -  to resolve such problems (after repairing malformed parts of the text). \<close>
    2.42 +  JVM). It is provided by the Isabelle Base plugin and enabled by default for
    2.43 +  all source files in Isabelle/jEdit. Sometimes such defaults are reset
    2.44 +  accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
    2.45 +  back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim
    2.46 +  ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its Unicode rendering
    2.47 +  ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/
    2.48 +  UTF-8-Isabelle\<close> helps to resolve such problems (after repairing malformed
    2.49 +  parts of the text). \<close>
    2.50  
    2.51  paragraph \<open>Font.\<close>
    2.52  text \<open>Correct rendering via Unicode requires a font that contains glyphs for