equal
deleted
inserted
replaced
213 |
213 |
214 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; |
214 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; |
215 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; |
215 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; |
216 |
216 |
217 fun attribute_setup name source comment = |
217 fun attribute_setup name source comment = |
218 ML_Lex.read_source false source |
218 ML_Lex.read_source source |
219 |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser" |
219 |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser" |
220 ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ |
220 ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ |
221 " parser " ^ ML_Syntax.print_string comment ^ ")") |
221 " parser " ^ ML_Syntax.print_string comment ^ ")") |
222 |> Context.proof_map; |
222 |> Context.proof_map; |
223 |
223 |