[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

On Sun, 29 Jul 2012, Makarius wrote:

> Here is a one-liner for private use in $ISABELLE_HOME_USER/ROOT:
>
>  session HOL-Test! in "~~/src/HOL" = Pure + theories Nat
>
> This works because $ISABELLE_HOME_USER is also a component.

Oops, the non-identifier name "HOL-Test" above needs to be quoted, 
according to the usual conventions of Isar outer syntax that is used for 
these config files:

   session "HOL-Test"! in "~~/src/HOL" = Pure + theories Nat


This lapse indicates another future issue, when session names shall be 
used to qualify theory names: we might have to change the global naming 
scheme to make them (long) identifiers without funny dashes.  Otherwise 
the qualification would not be usable within the term language, for 
example.


 	Makarius