eliminated old Method.add_method(s);
authorwenzelm
Sat May 30 15:00:23 2009 +0200 (2009-05-30 ago)
changeset 3130400a9c674cf40
parent 31303 4392ad427094
child 31305 a16f4d4f5b24
eliminated old Method.add_method(s);
NEWS
src/Pure/Isar/method.ML
     1.1 --- a/NEWS	Sat May 30 14:26:33 2009 +0200
     1.2 +++ b/NEWS	Sat May 30 15:00:23 2009 +0200
     1.3 @@ -26,6 +26,14 @@
     1.4  by the code generator; see Predicate.thy for an example.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Eliminated old Method.add_methods and related cominators for "method
    1.10 +args".  INCOMPATIBILITY, need to use simplified Method.setup
    1.11 +introduced in Isabelle2009.
    1.12 +
    1.13 +
    1.14 +
    1.15  New in Isabelle2009 (April 2009)
    1.16  --------------------------------
    1.17  
     2.1 --- a/src/Pure/Isar/method.ML	Sat May 30 14:26:33 2009 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Sat May 30 15:00:23 2009 +0200
     2.3 @@ -75,10 +75,6 @@
     2.4    val defined: theory -> string -> bool
     2.5    val method: theory -> src -> Proof.context -> method
     2.6    val method_i: theory -> src -> Proof.context -> method
     2.7 -  val add_methods: (bstring * (src -> Proof.context -> method) * string) list
     2.8 -    -> theory -> theory
     2.9 -  val add_method: bstring * (src -> Proof.context -> method) * string
    2.10 -    -> theory -> theory
    2.11    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    2.12    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    2.13    val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    2.14 @@ -343,6 +339,10 @@
    2.15      |> Pretty.chunks |> Pretty.writeln
    2.16    end;
    2.17  
    2.18 +fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
    2.19 +  #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
    2.20 +    handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
    2.21 +
    2.22  
    2.23  (* get methods *)
    2.24  
    2.25 @@ -363,27 +363,13 @@
    2.26  fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
    2.27  
    2.28  
    2.29 -(* add method *)
    2.30 -
    2.31 -fun add_methods raw_meths thy =
    2.32 -  let
    2.33 -    val new_meths = raw_meths |> map (fn (name, f, comment) =>
    2.34 -      (Binding.name name, ((f, comment), stamp ())));
    2.35 -
    2.36 -    fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths
    2.37 -      handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
    2.38 -  in Methods.map add thy end;
    2.39 -
    2.40 -val add_method = add_methods o Library.single;
    2.41 -
    2.42 -
    2.43  (* method setup *)
    2.44  
    2.45  fun syntax scan = Args.context_syntax "method" scan;
    2.46  
    2.47 -fun setup name scan comment =
    2.48 -  add_methods [(Binding.name_of name,
    2.49 -    fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)];
    2.50 +fun setup name scan =
    2.51 +  add_method name
    2.52 +    (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
    2.53  
    2.54  fun method_setup name (txt, pos) cmt =
    2.55    Context.theory_map (ML_Context.expression pos