Email Gateway (Aug 19 2022 at 14:12): Email Gateway (Aug 19 2022 at 14:12):From: Joachim Breitner <mail@joachim-breitner.de>
Dear List,
I’m currently in the phase where I make my theories nicely looking, and
I’m adding text. This means that I’m writing LaTeX code in text {* .. *}
blocks, and suddenly the automatic completion of abbreviations are very
annoying: I can’t enter, say \cite{foo}, without getting ∘te{foo}.
Since this is (I believe) a common use case I wonder if I am overlooking
something – can I make Isabelle/jEdit be smarter about this?
Is there maybe a way of entering a \ that prevents a following auto
completion? I tried “\\cite” (which would be a way that I would have
discovered without reading documentation), but that does not work.
(I guess I can disable auto completion in the options, but that’s 6
mouse clicks in the midst of a keyboard-only workflow, so I’d consider
that a work-around, no better than typing cite C-← \ C-→).
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:14):From: Makarius <makarius@sketis.net>
On Mon, 28 Apr 2014, Joachim Breitner wrote:
I’m currently in the phase where I make my theories nicely looking, and
I’m adding text. This means that I’m writing LaTeX code in text {* .. *}
blocks, and suddenly the automatic completion of abbreviations are very
annoying: I can’t enter, say \cite{foo}, without getting ∘te{foo}.
In Isabelle2013-2 the completion mechanism still lacks any context, so
what is good behaviour within the term language can easily become bad
behaviour in LaTeX source.
Some weeks ago, I have revisited the whole complex of completion once
again, and added a "language context" to address the above, but it is so
smart that it has other side-effects. This will still take a few more
weeks / months to consolidate for Isabelle2014 this summer.
Since this is (I believe) a common use case I wonder if I am overlooking
something – can I make Isabelle/jEdit be smarter about this?
Depends how much you want to invest. The mechanism reacts on key events
after filtering for the ones that insert plain text, ultimately it looks
at the buffer content independently how that was produce. So if you can
insert text without any critical key event, it will end up in the buffer
without completion. You can see this with plain C+c to copy from the main
cliboard register (there are several such registers). It does not help
though, to insert a \ by special means and then continue typing normally.
Alternatively, you can undo the accidental completion of \ci and then
continue typing, although there is an extra selection showing up that
needs to be canceled via ESC first. (I need to check if this is normal
jEdit behaviour, or an accident on the side of Isabelle/jEdit completion.)
I guess I can disable auto completion in the options, but that’s 6 mouse
clicks in the midst of a keyboard-only workflow, so I’d consider that a
work-around, no better than typing cite C-← \ C-).
It is sufficient to disable the option "jedit_completion_immediate".
Then you still have the popup-TAB mechanism for the term language.
Further hints on shortening GUI access paths are available on this recent
thread:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-April/msg00144.html
There might be even more possibilities via macros and/or BeanShell
scripting, but I am myself not an expert of all jEdit features.
Makarius
Email Gateway (Aug 19 2022 at 14:14):From: Joachim Breitner <breitner@kit.edu>
Hi,
a quite horrible workaround is adding
\catcode`\|=0 %
to your preamble, and then simply write your LaTeX commands with |
instead of \. It will break any real occurrence of | in the code and
look really strange, but at least your workflow is uninterrupted. If |
is not good, other characters might work.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:15):From: Makarius <makarius@sketis.net>
Low-level TeX hacking is normally not necessary in the Isabelle document
preparation system -- we stopped doing that 15 years ago.
Milner's meta-language is better suited for document programming than
Knuth's macro-language, i.e. you just make your own document antiquotation
@{cite NAME} with Isabelle syntax.
Just do a hypersearch for Thy_Output.antiquotation over all .ML and .thy
files of the Isabelle distribution to get some ideas.
$ISABELLE_HOME/src/Pure/Thy/rail.ML is a notable example that does not
pretty print formal entities, but emits LaTeX macros directly.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC