[isabelle-dev] Consolidation of manual naming

[Makarius]

On Thu, 3 Apr 2014, Florian Haftmann wrote:

>> Otherwise any reform of this little aministrative problem of Isabelle
>> repository versions is one of the build_doc command line: there is no
>> need to specify the session here, it could just name the
>> "document_variant" instead (but that would mean to rewrite the shell
>> script in Isabelle/Scala, where this information is available).
>
> Maybe at some time I would attempt such a rewrite as small Scala 
> exercise.

Getting acquainted with Isabelle/Scala is definitely a good thing.  The 
isabelle_scala_script wrapper makes it easy to get started without 
interference of the Pure.jar build process.

In this particular case I've accidentally done the work already, when 
passing by some other "doc" related details.  See bc61161a5bd0, which may 
also serve here is mini-tutorial how to convert a shell script into some 
Isabelle/Scala function.


> 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.)


 	Makarius