equal
deleted
inserted
replaced
206 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; |
206 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; |
207 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; |
207 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; |
208 |
208 |
209 fun attribute_setup name source comment = |
209 fun attribute_setup name source comment = |
210 ML_Lex.read_source false source |
210 ML_Lex.read_source false source |
211 |> ML_Context.expression (#range source) |
211 |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser" |
212 "val parser: Thm.attribute context_parser" |
|
213 ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ |
212 ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ |
214 " parser " ^ ML_Syntax.print_string comment ^ ")") |
213 " parser " ^ ML_Syntax.print_string comment ^ ")") |
215 |> Context.proof_map; |
214 |> Context.proof_map; |
216 |
215 |
217 |
216 |