On Fri, 2 May 2014, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
> text ‹
> @{term ‹A \un B›}
> ›
>
> Here the \un works as expected -- the cartouche remains intact
> independently of its
> content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un while
writing the above, the closing parenthesis are not there yet. The prover
sees something like
text {* @{term "A \un
lemma foo: "..." by ...
But why? In the ancient times, input was always sequential, as depth-first
traversal of the intended tree structure. In less ancient times, some people
proposed rigid structural editors to make it impossible to escape from nested
boxes (still seen today in TeXmacs), although that is a bit awkward. In the
past 10 years or so, the standard IDE approach has arrived somewhere in the
middle: the user is free to type intermediate non-sense, but the editor makes
it easy to get it right by default.
See also:
changeset: 56842:b6e266574b26
user: wenzelm
date: Sat May 03 20:31:29 2014 +0200
files: src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
description:
yet another completion option, to imitate old less ambitious behavior;
It allows to ignore the language context of the prover.
This is also an attempt to retain sanity, when masses of users complain
about having to learn new things in the coming release. Hopefully some
will do some actual testing of this big space of features, and report
problems before the release and not after it.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
