some actual workaround to remove document nodes;
authorwenzelm
Mon, 28 Jul 2014 11:03:28 +0200
changeset 590389ea92df3631a
parent 59037 f11f3d7589b1
child 59039 d1e9022c0175
some actual workaround to remove document nodes;
NEWS
src/Doc/JEdit/JEdit.thy
     1.1 --- a/NEWS	Sun Jul 27 15:40:19 2014 +0200
     1.2 +++ b/NEWS	Mon Jul 28 11:03:28 2014 +0200
     1.3 @@ -108,6 +108,9 @@
     1.4  * More support for remote files (e.g. http) using standard Java
     1.5  networking operations instead of jEdit virtual file-systems.
     1.6  
     1.7 +* Empty editors buffers that are no longer required (e.g.\ via theory
     1.8 +imports) are automatically removed from the document model.
     1.9 +
    1.10  * Improved Console/Scala plugin: more uniform scala.Console output,
    1.11  more robust treatment of threads and interrupts.
    1.12  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Jul 27 15:40:19 2014 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Jul 28 11:03:28 2014 +0200
     2.3 @@ -1662,11 +1662,11 @@
     2.4    \textbf{Workaround:} Copy/paste complete command text from
     2.5    elsewhere, or disable continuous checking temporarily.
     2.6  
     2.7 -  \item \textbf{Problem:} No way to delete document nodes from the overall
     2.8 +  \item \textbf{Problem:} No direct support to remove document nodes from the
     2.9    collection of theories.
    2.10  
    2.11 -  \textbf{Workaround:} Ignore unused files.  Restart whole
    2.12 -  Isabelle/jEdit session in worst-case situation.
    2.13 +  \textbf{Workaround:} Clear the buffer content of unused files and close
    2.14 +  \emph{without} saving changes.
    2.15  
    2.16    \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
    2.17    @{verbatim "C+MINUS"} for adjusting the editor font size depend on