Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Text-antiquotation: strange behavior

Email Gateway (Jul 06 2023 at 09:58):

From: Nicolas Meric <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle's users,

I have a strange behavior when processing a text-antiquotation.

Here is a small example that defines a text-antiquotation:

theory Test_Text_Antiquotation
  imports Main
begin

ML‹

fun check ctxt s pos name  =
  let
    val s' = Syntax.read_typ ctxt s
              |> Syntax.string_of_typ ctxt
              |> YXML.content_of
    val typ = Syntax.read_typ ctxt s      ― ‹<--- Works!›
    (val typ = Syntax.read_typ ctxt s') ― ‹<--- Fails!›
    val _ = if type_of name <> typ
            then error("Wrong type: " ^ (Syntax.string_of_term ctxt
name) ^ (Position.here pos))
            else ()
  in () end

val docitem_antiquotation_parser = Scan.lift Parse.embedded_input :
Input.source context_parser;

fun pretty_docitem_antiquotation_generic s ctxt src =
    let val (term,pos) = Input.source_content src
                        |> apfst (Syntax.read_term ctxt)
        val _ = check ctxt s pos term
    in  (Latex.text (Syntax.string_of_term ctxt term, pos))
    end

fun docitem_antiquotation bind typ =
 Document_Output.antiquotation_raw bind docitem_antiquotation_parser
(pretty_docitem_antiquotation_generic typ)

val _ = Theory.setup (docitem_antiquotation \<^binding>‹int› "int")
›

text‹@{int ‹2::int›}›

end

In the check function, if I use the string " s " to read the type for
the val " typ ",
then the parsing of the text-antiquotation in the text command works.

But if I use the string " s' ", then the parsing fails with the error:

Inner syntax error: unexpected end of input
Failed to parse type

If I use the code that generates the " s' " string
"outside" of a text-antiquotation context, everything works fine.

For example, when in an standard ML context, this code works:

ML‹
val ctxt = \<^context>
val s = "int"
val s' = Syntax.read_typ ctxt s
          |> Syntax.string_of_typ ctxt
          |> YXML.content_of
val typ = Syntax.read_typ ctxt s'
›

So, is this an expected behavior, or do I do something wrong?

Best regards.

Nicolas Méric

Last updated: Jan 04 2025 at 20:18 UTC