Theory Quote_Antiquote

theory Quote_Antiquote
imports Main
header {* \section{Concrete Syntax} *}

theory Quote_Antiquote imports Main begin

syntax
  "_quote"     :: "'b => ('a => 'b)"                ("(«_»)" [0] 1000)
  "_antiquote" :: "('a => 'b) => 'b"                ("´_" [1000] 1000)
  "_Assert"    :: "'a => 'a set"                    ("(\<lbrace>_\<rbrace>)" [0] 1000)

translations
  "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect «b»"

parse_translation {*
  let
    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(@{syntax_const "_quote"}, K quote_tr)] end
*}

end