src/Pure/Isar/attrib.ML
changeset 68823 5e7b1ae10eb8
parent 68816 5a53724fe247
child 69187 d8849cfad60f
equal deleted inserted replaced
68822:253f04c1e814 68823:5e7b1ae10eb8
   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