On Mon, 7 Apr 2014, Florian Haftmann wrote:
Nevertheless I still think its a good idea to spend half an hour to
establish a more strict name correspondance while keeping the
(lowercase) document names stable, e.g.
foo-bar <-:-> Foo_Bar
I now see b266e7a86485 with foo-bar <-:-> Foo-Bar.
It is still unclear to me what the actual confusion was, and what is the
improvement. A "-" within a session name is obsolete for a long time --
it is in conflict with session-qualified theory names and plain long_id
token syntax. (That is not very relevant for Doc sessions, though.)
When inspecting the ROOT file I saw the session name for »ZF-Logics« and
gave that some authority.
Maybe it is best if I will move on »ZF_Logics« etc. in yet another
iteration to get rid of these historic names. At least that made the
confusion apparent.
I still don't understand what the confusion actually is. These things are
really old, especially the "logics" manuals, which used to be just one
latex document a long time ago. It is not always possible to have
immediately obvious canonical names for everything -- there are often
conflicting side-conditions etc.
We do have a tradition to get things right eventually, but for that there
needs to be a clear direction, and some level of significance for a change
to be considered: it needs 2-3 good reasons, not just half a reason.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
