src/Pure/Isar/method.ML
changeset 59914 d1ddcd8df4e4
parent 59909 fbf4d5ad500d
child 59917 9830c944670f
equal deleted inserted replaced
59913:a7f6359665c6 59914:d1ddcd8df4e4
   370   in #1 o Name_Space.check context (get_methods context) end;
   370   in #1 o Name_Space.check context (get_methods context) end;
   371 
   371 
   372 fun check_src ctxt =
   372 fun check_src ctxt =
   373   #1 o Token.check_src ctxt (get_methods (Context.Proof ctxt));
   373   #1 o Token.check_src ctxt (get_methods (Context.Proof ctxt));
   374 
   374 
       
   375 fun checked_info ctxt name =
       
   376   let val space = Name_Space.space_of_table (get_methods (Context.Proof ctxt))
       
   377   in (Name_Space.kind_of space, Name_Space.markup space name) end;
       
   378 
   375 
   379 
   376 (* method setup *)
   380 (* method setup *)
   377 
   381 
   378 fun method_syntax scan src ctxt : method =
   382 fun method_syntax scan src ctxt : method =
   379   let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
   383   let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
   572     val (meth_name, mk_src) =
   576     val (meth_name, mk_src) =
   573       (case check_ctxt of
   577       (case check_ctxt of
   574         NONE => (Parse.xname, Token.src)
   578         NONE => (Parse.xname, Token.src)
   575       | SOME ctxt =>
   579       | SOME ctxt =>
   576          (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
   580          (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
   577           fn name => fn args => check_src ctxt (Token.src name args)));
   581           fn (name, pos) => fn args => Token.src_checked (name, pos) args (checked_info ctxt name)));
   578 
   582 
   579     fun meth5 x =
   583     fun meth5 x =
   580      (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||
   584      (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||
   581       Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
   585       Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
   582         Source (mk_src ("cartouche", Token.pos_of tok) [tok])) ||
   586         Source (mk_src ("cartouche", Token.pos_of tok) [tok])) ||
   584     and meth4 x =
   588     and meth4 x =
   585      (meth5 -- Parse.position (Parse.$$$ "?")
   589      (meth5 -- Parse.position (Parse.$$$ "?")
   586         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
   590         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
   587       meth5 -- Parse.position (Parse.$$$ "+")
   591       meth5 -- Parse.position (Parse.$$$ "+")
   588         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
   592         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
   589       meth5 --
   593       meth5 -- (Parse.position (Parse.$$$ "[") --
   590         (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
   594           Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
   591         >> (fn (m, (((_, pos1), n), (_, pos2))) =>
   595         >> (fn (m, (((_, pos1), n), (_, pos2))) =>
   592             Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
   596             Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
   593       meth5) x
   597       meth5) x
   594     and meth3 x =
   598     and meth3 x =
   595      (Parse.position meth_name -- Parse.args1 is_symid_meth >> (Source o uncurry mk_src) ||
   599      (Parse.position meth_name -- Parse.args1 is_symid_meth >> (Source o uncurry mk_src) ||