[isabelle-dev] Two problems

[Makarius]

On Mon, 3 Dec 2012, Lawrence Paulson wrote:

> Surely the existence of two theories of the same name can be detected?

The deeper problem here is that theories still have the ancient flat name 
space.  So the file-system paths in the source are ultimately stripped to 
the base name when doing comparisons.


We are still moving (extremely slowly) towards fully-qualified theory 
names of the form SESSION.THEORY, e.g. "HOL.Main", "HOLCF.HOLCF" with some 
ways to omit the prefix within the same session, say.

The isabelle build reform from this summer already introduces an authentic 
name space for (unqualified) session names.

Here are some of the remaining obstacles to prefix session names to theory 
names:

   * Too many ways to manage theory dependencies.  There are old and new
     theory loader variants and combinations: isabelle tty, build, emacs,
     jedit all do it slightly differently.  Ultimately, I would like to see
     just one way in Isabelle/Scala, and even Proof General would use that
     without taking notice.

   * Proof tools that assume that the long names for formal entities look
     like this:

       THEORY.NAME
       THEORY.LOCALE.NAME

     Larry himself introduced this assumption some years ago, but it was
     not there in 1998 when I introduced the name space concept in
     Isabelle.  ML tools should not guess at the layout of full names.
     This is an abstract datatype that happens to be implemented as
     "string" for historical reasons.


 	Makarius