src/Pure/Isar/method.ML
changeset 22846 fb79144af9a3
parent 22586 d2008c5f8d99
child 23086 12320f6e2523
     1.1 --- a/src/Pure/Isar/method.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -378,28 +378,24 @@
     1.4  (* method definitions *)
     1.5  
     1.6  structure MethodsData = TheoryDataFun
     1.7 -(struct
     1.8 -  val name = "Isar/methods";
     1.9 +(
    1.10    type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
    1.11 -
    1.12    val empty = NameSpace.empty_table;
    1.13    val copy = I;
    1.14    val extend = I;
    1.15    fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
    1.16      error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
    1.17 +);
    1.18  
    1.19 -  fun print _ meths =
    1.20 -    let
    1.21 -      fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.22 -        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.23 -    in
    1.24 -      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    1.25 -      |> Pretty.chunks |> Pretty.writeln
    1.26 -    end;
    1.27 -end);
    1.28 -
    1.29 -val _ = Context.add_setup MethodsData.init;
    1.30 -val print_methods = MethodsData.print;
    1.31 +fun print_methods thy =
    1.32 +  let
    1.33 +    val meths = MethodsData.get thy;
    1.34 +    fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.35 +      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.36 +  in
    1.37 +    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    1.38 +    |> Pretty.chunks |> Pretty.writeln
    1.39 +  end;
    1.40  
    1.41  
    1.42  (* get methods *)