73 val print_methods: theory -> unit |
73 val print_methods: theory -> unit |
74 val intern: theory -> xstring -> string |
74 val intern: theory -> xstring -> string |
75 val defined: theory -> string -> bool |
75 val defined: theory -> string -> bool |
76 val method: theory -> src -> Proof.context -> method |
76 val method: theory -> src -> Proof.context -> method |
77 val method_i: theory -> src -> Proof.context -> method |
77 val method_i: theory -> src -> Proof.context -> method |
78 val add_methods: (bstring * (src -> Proof.context -> method) * string) list |
|
79 -> theory -> theory |
|
80 val add_method: bstring * (src -> Proof.context -> method) * string |
|
81 -> theory -> theory |
|
82 val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context |
78 val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context |
83 val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory |
79 val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory |
84 val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> |
80 val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> |
85 theory -> theory |
81 theory -> theory |
86 type modifier = (Proof.context -> Proof.context) * attribute |
82 type modifier = (Proof.context -> Proof.context) * attribute |
340 [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
336 [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
341 in |
337 in |
342 [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))] |
338 [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))] |
343 |> Pretty.chunks |> Pretty.writeln |
339 |> Pretty.chunks |> Pretty.writeln |
344 end; |
340 end; |
|
341 |
|
342 fun add_method name meth comment thy = thy |> Methods.map (fn meths => |
|
343 #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths) |
|
344 handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup)); |
345 |
345 |
346 |
346 |
347 (* get methods *) |
347 (* get methods *) |
348 |
348 |
349 val intern = NameSpace.intern o #1 o Methods.get; |
349 val intern = NameSpace.intern o #1 o Methods.get; |
361 in meth end; |
361 in meth end; |
362 |
362 |
363 fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy))); |
363 fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy))); |
364 |
364 |
365 |
365 |
366 (* add method *) |
|
367 |
|
368 fun add_methods raw_meths thy = |
|
369 let |
|
370 val new_meths = raw_meths |> map (fn (name, f, comment) => |
|
371 (Binding.name name, ((f, comment), stamp ()))); |
|
372 |
|
373 fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths |
|
374 handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup); |
|
375 in Methods.map add thy end; |
|
376 |
|
377 val add_method = add_methods o Library.single; |
|
378 |
|
379 |
|
380 (* method setup *) |
366 (* method setup *) |
381 |
367 |
382 fun syntax scan = Args.context_syntax "method" scan; |
368 fun syntax scan = Args.context_syntax "method" scan; |
383 |
369 |
384 fun setup name scan comment = |
370 fun setup name scan = |
385 add_methods [(Binding.name_of name, |
371 add_method name |
386 fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)]; |
372 (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end); |
387 |
373 |
388 fun method_setup name (txt, pos) cmt = |
374 fun method_setup name (txt, pos) cmt = |
389 Context.theory_map (ML_Context.expression pos |
375 Context.theory_map (ML_Context.expression pos |
390 "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" |
376 "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" |
391 "Context.map_theory (Method.setup name scan comment)" |
377 "Context.map_theory (Method.setup name scan comment)" |