[isabelle-dev] Unification of doc sessions vs. doc names

[Makarius]

On Sat, 22 Sep 2012, Florian Haftmann wrote:

> Currently, we have still the ancient walking-by of doc sessions (e.g. 
> IsarImplementation – note the CaMeL case) and corresponding document 
> names (e.g. implementation).  Is there anything speaking against 
> unifying these now?

When I turned doc-src into more regular src/Doc some weeks ago, I 
remembered that you have pointed out this question before, but I did not 
see yet a direction where to move.


If you take the session IsarRef and its resulting document isar-ref, it is 
both fairly non-standard.  A proper session name would be Isar_Ref.

Or one could de-unifiy things with the other sessions and call it isar_ref 
in conformance with its isar_ref.pdf.  This would simplify the situation 
in "isabelle build_doc", but deviate from normal session naming and 
existing public names like http://isabelle.in.tum.de/doc/isar-ref.pdf

To add more to the confusion, there are also some regular sessions that 
produce some manual:

   * HOL-SPARK-Manual with regular document.pdf
   * Collections (AFP) with document.pdf and userguide.pdf

All these variants have good reasons to exisit. Where is the general 
direction to move?  I don't see it yet.


 	Makarius