[isabelle-dev] NEWS: session-qualified theory imports

[Makarius]

*** General ***

* Theory names are qualified by the session name that they belong to.
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).


This refers to Isabelle/1a73ad1c06dd. It is the outcome of struggling
with many unexpected problems and corner cases. We have quite some
complexity (or complication) in AFP, with various adhoc sessions with
overlapping sources.

Hopefully it now works smoothly. In any case, the coming weeks before
the Isabelle2017 release are there to consolidate it beyond doubt.


	Makarius