Email Gateway (Sep 05 2020 at 15:00): Email Gateway (Sep 05 2020 at 15:00):From: Walther Neuper <walther.neuper@jku.at>
reading isar-ref.pdf and src/Pure gives me the impression, that
cartouches are NOT designed to contain outer syntax.
Is that impression correct?
If "yes", then I'll proceed with implementation.pdf "§3. Concrete syntax
and type-checking",
if "no": please, point me to an example, where a cartouche contains
outer syntax.
Many thanks in advance,
Walther
Email Gateway (Sep 05 2020 at 21:03):From: Makarius <makarius@sketis.net>
Here is an example that contains outer syntax keywords:
text ‹
@{theory_text ‹term x›}
›
You can use C-hover click on "theory_text" to see how it is implemented (as
text antiquotation).
Of course, you can use embedded cartouches in other languages as well.
Makarius
Email Gateway (Sep 06 2020 at 07:03):From: Walther Neuper <walther.neuper@jku.at>
On 05.09.20 23:03, Makarius wrote:
On 05/09/2020 16:59, Walther Neuper wrote:
reading isar-ref.pdf and src/Pure gives me the impression, that
cartouches are NOT designed to contain outer syntax.
[...]
Here is an example that contains outer syntax keywords:text ‹
@{theory_text ‹term x›}
›You can use C-hover click on "theory_text" to see how it is implemented (as
text antiquotation).Of course, you can use embedded cartouches in other languages as well.
Makarius
Thank you!
So it's next to find out, why
text ‹ @{theory_text ‹ ISAC ‹ Problem ("Biegelinie", ["Biegelinien"])
"y x = q_0 * L ^ 2 / (4 * EI)" › ›} ›
does not render quoted text red the same way as it is done with
"immediate" theory_text, e.g.
ISAC ‹
Problem ("Biegelinie", ["Biegelinien"])
"y x = q_0 * L ^ 2 / (4 * EI)"
›
in the theory body without further surroundings given the definition
val _ = Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC
language" ((Parse.input Parse.cartouche) >> (fn input => Toplevel.keep
(fn _ => ignore (ML_Lex.read_source input))))
Good training in how to read and investigate Isabelle code.
Walther
Email Gateway (Sep 06 2020 at 20:57):From: Makarius <makarius@sketis.net>
This is because the @{theory_text} document antiquotation only takes the outer
syntax tokens into account; there is no evaluation of commands, and thus no
markup from the command semantics.
The included definition of @{theory_commands} improves on this in an adhoc
manner, using Outer_Syntax.parse_text and Toplevel.command_exception --- this
basically works, but causes some duplication of markup.
Before I do the usual fine-tuning to get PIDE markup to the point, without
duplicates: Can you say what your actual application is? Do you need a
document antiquotation at all, or something else?
Makarius
Email Gateway (Sep 07 2020 at 10:32):From: Walther Neuper <walther.neuper@jku.at>
On 06.09.20 22:56, Makarius wrote:
On 06/09/2020 09:03, Walther Neuper wrote:
So it's next to find out, why
text ‹ @{theory_text ‹ ISAC ‹ Problem ("Biegelinie", ["Biegelinien"])
"y x = q_0 * L ^ 2 / (4 * EI)" › ›} ›
does not render quoted text red the same way as it is done with
"immediate" theory_text, e.g.
ISAC ‹
Problem ("Biegelinie", ["Biegelinien"])
"y x = q_0 * L ^ 2 / (4 * EI)"
›
in the theory body without further surroundings given the definition
thank you for the explanation of how the antiquotation works ..
This is because the @{theory_text} document antiquotation only takes the outer
syntax tokens into account; there is no evaluation of commands, and thus no
markup from the command semantics.
.. and the hints for continuing that way ..
The included definition of @{theory_commands} (*) improves on this in an adhoc
manner, using Outer_Syntax.parse_text and Toplevel.command_exception --- this
basically works, but causes some duplication of markup.Before I do the usual fine-tuning to get PIDE markup to the point, without
duplicates:
... but I suppose now, that it will be more straight forward to go to
inner syntax directly:
Can you say what your actual application is? Do you need a
document antiquotation at all, or something else?
We need a cartouche like ISAC above, where the cartouche contains a
specific format of forward proof (a variant of Back's "structured
derivation") initalised by an explicit formal specification of
pre-condition and post-condition (within the same cartouche).
Thus now I plan to follow implementation.pdf §3."Concrete syntax and
type-checking" and investigate Isabelle's standard code dealing with
"proof" in order to provide semantics to new keywords in inner syntax.
Thank you for all,
Walther
PS(*): cannot find "theory_commands" at the actual
https://isabelle.in.tum.de/repos/isabelle; but there is
"local_theory_command" with "local_theory_to_proof" which sounds promising.
PPS: Following your hint at the Isabelle workshop, to study
Isabelle_Naproche, I am impressed by the many new possibilities (e.g.
delegate parsing via Isabelle server) which we are not going to fully
exploit in this phase of development.
Email Gateway (Sep 07 2020 at 17:05):From: Makarius <makarius@sketis.net>
Oops, I've forgotten the attached theory.
Makarius
Theory_Commands.thy
Email Gateway (Sep 08 2020 at 10:10):From: Walther Neuper <walther.neuper@jku.at>
thank you, the theory looks interesting, while I don't really understand
the details --- so it's hard for me to decide whether to place parsing
and interpreting in outer syntax or in inner syntax.
Before I come up with the many questions I already see, I'll go into
trials with inner syntax for some time.
Walther
Last updated: Jan 04 2025 at 20:18 UTC