Stream: Isabelle/ML

Topic: antiquotation embedded

view this post on Zulip Kevin Kappelmann (Sep 30 2021 at 13:07):

In ML_Antiquotation, what's the meaning of embedded? How do I decide, for example, if I should pick inline or inline_embedded to set up my antiquotation?

  val declaration: binding -> 'a context_parser ->
    (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) ->
    theory -> theory
  val declaration_embedded: binding -> 'a context_parser ->
    (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) ->
    theory -> theory
  val inline: binding -> string context_parser -> theory -> theory
  val inline_embedded: binding -> string context_parser -> theory -> theory
  val value: binding -> string context_parser -> theory -> theory
  val value_embedded: binding -> string context_parser -> theory -> theory

Last updated: Nov 05 2025 at 08:30 UTC