Re: [isabelle-dev] Consolidation of manual naming

2014-04-11 Thread Florian Haftmann
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

Re: [isabelle-dev] Consolidation of manual naming

2014-04-11 Thread Tobias Nipkow
I consider this twofold renaming of directories pointless, and as you know, it required a twofold update in some other theories of mine. I guess I should have stated my displeasure earlier but thought that since Makarius had already stated he didn't even see the problem, this would discourage you.

Re: [isabelle-dev] Consolidation of manual naming

2014-04-10 Thread Makarius
On Mon, 7 Apr 2014, Makarius wrote: 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

Re: [isabelle-dev] Consolidation of manual naming

2014-04-09 Thread Makarius
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

Re: [isabelle-dev] Consolidation of manual naming

2014-04-08 Thread Florian Haftmann
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. See now http://isabelle.in.tum.de/reports/Isabelle/rev/856492b0f755 Florian -- PGP available:

Re: [isabelle-dev] Consolidation of manual naming

2014-04-07 Thread 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

Re: [isabelle-dev] Consolidation of manual naming

2014-04-07 Thread Florian Haftmann
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

Re: [isabelle-dev] Consolidation of manual naming

2014-04-03 Thread Florian Haftmann
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,

Re: [isabelle-dev] Consolidation of manual naming

2014-03-28 Thread Makarius
On Wed, 26 Mar 2014, Florian Haftmann wrote: since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be worth an effort to consolidate this? I regularly get confused about that. This is one of these recurrent (low

Re: [isabelle-dev] Consolidation of manual naming

2014-03-28 Thread Makarius
On Fri, 28 Mar 2014, Makarius wrote: So what is actually the problem here? The main practical situation where this connection of divergent names needs to be resolved is isabelle build_doc. That could be smarter, or actually somehow be automatic as part of the document viewer. But we are

[isabelle-dev] Consolidation of manual naming

2014-03-26 Thread Florian Haftmann
Hi, since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be worth an effort to consolidate this? I regularly get confused about that. Cheers, Florian -- PGP available:

Re: [isabelle-dev] Consolidation of manual naming

2014-03-26 Thread Johannes Hölzl
+1 Fortunately, nowadays the list of manuals shown in jEdit is very helpful here. Am Mittwoch, den 26.03.2014, 22:07 +0100 schrieb Florian Haftmann: Hi, since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be