# HG changeset patch
# User wenzelm
# Date 1503089724 -7200
# Node ID 1a73ad1c06dd41a4590a864661dfc4c3d7a5e4e1
# Parent  cc19f7ca2ed6f49c1e8b8e551c0f76e95d7aa7a1
more NEWS;

diff -r cc19f7ca2ed6 -r 1a73ad1c06dd NEWS
--- a/NEWS	Fri Aug 18 20:47:47 2017 +0200
+++ b/NEWS	Fri Aug 18 22:55:24 2017 +0200
@@ -23,14 +23,22 @@
 modules around a Language Server implementation.
 
 * Theory names are qualified by the session name that they belong to.
-This affects imports, but not the theory name space prefix: it remains
-the theory base name as before. In order to import theories from other
-sessions, the ROOT file format provides a new 'sessions' keyword. In
-contrast, a theory that is imported in the old-fashioned manner via an
-explicit file-system path belongs to the current session.
-
-Theories that are imported from other sessions are excluded from the
-current session document.
+This affects imports, but not the theory name space prefix (which is
+just the theory base name as before).
+
+In order to import theories from other sessions, the ROOT file format
+provides a new 'sessions' keyword. In contrast, a theory that is
+imported in the old-fashioned manner via an explicit file-system path
+belongs to the current session, and might cause theory name confusion
+later on. Theories that are imported from other sessions are excluded
+from the current session document. The command-line tool "isabelle
+imports" helps to update theory imports.
+
+Properly qualified imports allow the Prover IDE to process arbitrary
+theory hierarchies independently of the underlying logic session image
+(e.g. option "isabelle jedit -l"), but the directory structure needs to
+be known in advance (e.g. option "isabelle jedit -d" or a line in the
+file $ISABELLE_HOME_USER/ROOTS).
 
 * The main theory entry points for some non-HOL sessions have changed,
 to avoid confusion with the global name "Main" of the session HOL. This