Am 17/04/2012 16:13, schrieb Makarius: > On Tue, 17 Apr 2012, Tobias Nipkow wrote: >> and would also leave room for an ASCII syntax for \<leftrightarrow> (namely >> <->). > > Using <--> for <-> and making room for another <-> would also mean that the > user > has to type/read the longer unwieldy sequence by default.
Calling "--" as opposed to "-" unwieldy is a bit of a joke. And provided the editor supports the conversion to proper symbols nicely, it is merely a question of typing, not reading. > Anyway, what is the role of the ASCII replacement syntax today? We use it > both > for prover syntax and input methods of the editor, which I always find > difficult > to explain to new users. I have not experienced those difficulties. > In practice the alternative ASCII input is mainly > passed to the prover because the editor completion mechanisms are still > require > an effort to change focus and press extra keys. Not in ProofGeneral. I type --> and it becomes \<longrightarrow>. > A really smooth input method in the editor could overcome the need for ASCII > replacement syntax altogether. Such input method could also admit multiple > associations, e.g the user typing short <-> would get a selection of arrows to > be inserted into the text. This is what I would call unwieldy: instead of typing <--> or <-> (and having them converted to the appropriate symbols) you always type <->, but then you have to select from a menue. I don't see the progress. > I have seen pretty good mathematical input methods somewhere before, maybe in > TeXmacs, maybe in some computer-algebra system. I checked out TeXmacs and, surprise, surprise, when you type <-> it is converted into \leftrightarrow, and when you type <--> it becomes \longleftrightarrow. Tobias > This would mean a conceptual > advance, not just a variation of old conventions. I.e. we could overcome > alternative syntax tables eventually. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
