src/Tools/jEdit/README.html

   <em>asynchronous document processing</em>, which is supported
   natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
 </p>
 
 <p>
-  <b>Isabelle/jEdit</b> is the main example application within the PIDE
+  <b>Isabelle/jEdit</b> is the flagship application of the PIDE
   framework &mdash; it illustrates many of the ideas in a realistic
   manner, ready to be used right now in Isabelle applications.
 </p>
 
 <p>

 (<tt>CONTROL</tt> on Linux or Windows,
   <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
 
 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
   windows by jEdit, which also allows multiple instances.</li>
+
+<li>Formal output (tooltips etc.) may be explored recursively, using the
+same techniques as in the editor source buffer.</li>
 
 <li>Prover process and source files are managed by the Isabelle/Scala on
 the editor side.  The prover experiences a mostly timeless and
 stateless environment of formal document content.</li>
 

     seen on the screen (or printer).
   </li>
 
   <li>Input methods:
     <ul>
+      <li>use the Symbols dockable</li>
       <li>copy/paste from decoded source files</li>
       <li>copy/paste from prover output</li>
       <li>completion provided by Isabelle plugin, e.g.<br/>
 
       <table border="1">