--- a/NEWS Tue Dec 12 17:47:23 2017 +0100
+++ b/NEWS Tue Dec 12 17:46:22 2017 +0100
@@ -87,8 +87,12 @@
more accurately: only terminal proof steps ('by' etc.) are skipped.
* Command-line tool "isabelle document" has been re-implemented in
-Isabelle/Scala, with simplified arguments and explicit errors from the
-latex process. Minor INCOMPATIBILITY.
+Isabelle/Scala, with simplified arguments. Minor INCOMPATIBILITY.
+
+* Original source positions are inlined into generated tex files: this
+improves error messages by "isabelle document", but may sometimes
+confuse LaTeX. Rare INCOMPATIBILITY, set option
+"document_positions=false" to avoid this.
*** HOL ***