equal
deleted
inserted
replaced
104 |
104 |
105 subsubsection {* Further nesting: antiquotations *} |
105 subsubsection {* Further nesting: antiquotations *} |
106 |
106 |
107 setup -- "ML antiquotation" |
107 setup -- "ML antiquotation" |
108 {* |
108 {* |
109 ML_Antiquote.inline @{binding term_cartouche} |
109 ML_Antiquotation.inline @{binding term_cartouche} |
110 (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
110 (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> |
111 (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
111 (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) |
112 *} |
112 *} |
113 |
113 |
114 setup -- "document antiquotation" |
114 setup -- "document antiquotation" |