Re: [isabelle-dev] NEWS: document preparation refinements
On Mon, 26 Oct 2015, Tobias Nipkow wrote:
On 23/10/2015 23:16, Makarius wrote:
* The @{text} antiquotation now ignores the antiquotation option
"source". The given text content is output unconditionally, without any
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
argument where they are really intended, e.g. @{text ‹"foo"›}. Initial
or terminal spaces are ignored.
I have wanted the surrounding quotes that come with [source] to go away since
day 1. Unfortunately the above change does not solve my `problem': I have
many occurrences of @{term[source]} where I have to remove " explicitly by
wrapping my own \noquotes macro around it.
I know.
The reason why @{text} no longer prints the source quotes is that it is no
longer a member of the class of "standard" antiquotations @{typ},
@{term}, {prop}, @{thm}. Instead it does its own well-defined business.
The standard antiquotations like @{term} did not change so far, and
require more thoughts in the future. Inlining formal material into the
generated document needs to be done differently, such that it fits with
the PIDE document model of semantic markup.
Morover, the use of double quote notation itself is gradually on retreat:
more and more cartouches show up in syntax definitions.
Cartouches have many advantages. E.g. there is a clear concept to add or
remove a level of cartouche quotation, without having to worry about
escaped quotes in the body.
A disadvantage is that cartouches everywhere (with lots of nesting) look
more boring than varying quotes, a bit like LISP. Or is that modesty in
syntax an advantage as well?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: document preparation refinements
Thanks, that did the trick. Tobias On 26/10/2015 18:16, Makarius wrote: On Sat, 24 Oct 2015, Tobias Nipkow wrote: I don't know if this is related, but it must have happened recently: The [display] option for antiquotations now (eg 436b7fe89cdc) generates latex that indents the text following the display, even if there is no newline in between. This is in contrast to latex conventions (eg \[ \]) and I would rather not have to insert lots of \nondent by hand. There is indeed one \n too much, which may produce an unintended paragraph in LaTeX. I've changed that as follows: changeset: 61516:8e3705d91cfa tag: tip user:wenzelm date:Mon Oct 26 18:04:17 2015 +0100 summary: clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display]; Makarius smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: document preparation refinements
On Sat, 24 Oct 2015, Tobias Nipkow wrote: I don't know if this is related, but it must have happened recently: The [display] option for antiquotations now (eg 436b7fe89cdc) generates latex that indents the text following the display, even if there is no newline in between. This is in contrast to latex conventions (eg \[ \]) and I would rather not have to insert lots of \nondent by hand. There is indeed one \n too much, which may produce an unintended paragraph in LaTeX. I've changed that as follows: changeset: 61516:8e3705d91cfa tag: tip user:wenzelm date:Mon Oct 26 18:04:17 2015 +0100 summary: clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display]; Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: document preparation refinements
Some more NEWS items (Isabelle/436b7fe89cdc):
*** Document preparation ***
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>‹...› is equivalent to @{name ‹...›} and
‹...› without control symbol is equivalent to @{cartouche ‹...›}. The
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "▩", "∗", "❙".
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
Consequently, ‹...› without any decoration prints literal quasi-formal
text. Command-line tool "isabelle update_cartouches -t" helps to update
old sources, by approximative patching of the content of string and
cartouche tokens seen in theory sources.
* The @{text} antiquotation now ignores the antiquotation option
"source". The given text content is output unconditionally, without any
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
argument where they are really intended, e.g. @{text ‹"foo"›}. Initial
or terminal spaces are ignored.
Makarius___
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
