Re: [isabelle-dev] code abbreviation for mapping over a fixed range
This email refers to the following commit: http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 code abbreviation for mapping over a fixed range Is there a specific reason for this code equation: "map_range f (Suc n) = map_range f n @ [f n]" It seems rather inefficient. Anyway, what's the purpose of "map_range". cheers chris PS: I was confused about [code_abbrev], thus looked it up in isar-ref, then was further confused :D "code_abbrev" declares (or with option “del” removes) equations which are applied as rewrite rules to any result of an evaluation and symmetrically during preprocessing to any code equation or evaluation input. In my opinion the usage of the word "symmetrically" could be clarified. Does it mean "similar to the previous use case" or "symmetric in the sense of reading the equation from right to left"? signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: document preparation refinements
*** General ***
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>‹...› is equivalent to @{name ‹...›}.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
instead of former C+e LEFT.
*** Document preparation ***
* HTML presentation uses the standard IsabelleText font and Unicode
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
print mode "HTML" looses its special meaning.
* Commands 'paragraph' and 'subparagraph' provide additional section
headings. Thus there are 6 levels of standard headings, as in HTML.
* Text is structured in paragraphs and nested lists, using notation that
is similar to Markdown. The control symbols for list items are as
follows:
▪ itemize
▸ enumerate
➧ description
* Text may contain control symbols for markup and formatting as follows:
⇤ \noindent
┈ \smallskip
┉ \medskip
━ \bigskip
* Command 'text_raw' has been clarified: input text is processed as in
'text' (with antiquotations and control symbols). The key difference is
the lack of the surrounding isabelle markup environment in output.
* Document antiquotations @{emph} and @{bold} output LaTeX source
recursively, adding appropriate text style markup. These are typically
used in the short form ∗‹...› and ❙‹...›.
All this refers e.g. to Isabelle/dcc8e1d34b18. The general trend is to
make the editor view, LaTeX output and HTML output converge eventually,
although we are still far from that.
Examples for the Markdown paragraph/list notation and other control
symbols can be seen in src/Doc: Implementation, Isar_Ref, JEdit, System.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: editor reactivity and State panel
*** Prover IDE -- Isabelle/Scala/jEdit *** * Improved scheduling for urgent print tasks (e.g. command state output, interactive queries) wrt. long-running background tasks. * The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. Option "editor_output_state" controls implicit proof state output in the Output panel: suppressing this reduces resource requirements of prover time and GUI space. * The text overview column (status of errors, warnings etc.) is updated asynchronously, leading to much better editor reactivity. Moreover, the full document node content is taken into account. E.g. see current Isabelle/3590367b0ce9. These NEWS items are already there for some time. Taken together they might help in situations of really big proof states, to request output manually on demand. The text overview painting is only related to the general theme to manage things more asynchronously for improved reactivity. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
