--- a/NEWS Wed Nov 20 16:43:09 2013 +0100
+++ b/NEWS Wed Nov 20 17:00:49 2013 +0100
@@ -4,6 +4,12 @@
New in this Isabelle version
----------------------------
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
+Open text buffers take precedence over copies within the file-system.
+
+
*** HOL ***
* Qualified constant names Wellfounded.acc, Wellfounded.accp.
--- a/src/Doc/JEdit/JEdit.thy Wed Nov 20 16:43:09 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Nov 20 17:00:49 2013 +0100
@@ -1064,12 +1064,6 @@
text {*
\begin{itemize}
- \item \textbf{Problem:} Lack of dependency management for auxiliary files
- that contribute to a theory (e.g.\ @{command ML_file}).
-
- \textbf{Workaround:} Re-load files manually within the prover, by
- editing corresponding command in the text.
-
\item \textbf{Problem:} Odd behavior of some diagnostic commands with
global side-effects, like writing a physical file.