removed help_methods;
authorwenzelm
Sat Jul 01 19:45:23 2000 +0200 (2000-07-01)
changeset 922292ad2341179d
parent 9221 e1fd1003d5f9
child 9223 eb752c2fac22
removed help_methods;
tuned print_methods;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Sat Jul 01 19:44:57 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Jul 01 19:45:23 2000 +0200
     1.3 @@ -53,7 +53,6 @@
     1.4    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
     1.5    val tactic: string -> Proof.context -> Proof.method
     1.6    exception METHOD_FAIL of (string * Position.T) * exn
     1.7 -  val help_methods: theory option -> Pretty.T list
     1.8    val method: theory -> Args.src -> Proof.context -> Proof.method
     1.9    val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string -> theory -> theory
    1.10    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    1.11 @@ -379,24 +378,19 @@
    1.12        meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
    1.13          error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
    1.14  
    1.15 -  fun pretty_meths verbose {space, meths} =
    1.16 +  fun print _ {space, meths} =
    1.17      let
    1.18        fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.19          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.20      in
    1.21 -      (if not verbose then [] else [Display.pretty_name_space ("method name space", space)]) @
    1.22        [Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))]
    1.23 +      |> Pretty.chunks |> Pretty.writeln
    1.24      end;
    1.25 -
    1.26 -  fun print _ = Pretty.writeln o Pretty.chunks o pretty_meths true;
    1.27  end;
    1.28  
    1.29  structure MethodsData = TheoryDataFun(MethodsDataArgs);
    1.30  val print_methods = MethodsData.print;
    1.31  
    1.32 -fun help_methods None = [Pretty.str "methods: (unkown theory context)"]
    1.33 -  | help_methods (Some thy) = MethodsDataArgs.pretty_meths false (MethodsData.get thy);
    1.34 -
    1.35  
    1.36  (* get methods *)
    1.37