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-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 unders

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 pas

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

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: http://home.informatik.tu-mue

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 w

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 rewr

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/Scal

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 t

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 p

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

[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: http://home.informatik.tu-muenchen.de/