[isabelle-dev] Consolidation of manual naming
makarius at sketis.net
Mon Apr 7 17:15:08 CEST 2014
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
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
> 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.)
More information about the isabelle-dev