print_help;
authorwenzelm
Thu Aug 26 19:01:58 1999 +0200 (1999-08-26)
changeset 7367a79d4683fadf
parent 7366 22a64baa7013
child 7368 6b1b6b7c1df0
print_help;
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 26 19:01:22 1999 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 26 19:01:58 1999 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4  signature ATTRIB =
     1.5  sig
     1.6    include BASIC_ATTRIB
     1.7 +  val help_attributes: theory -> unit
     1.8    exception ATTRIB_FAIL of (string * Position.T) * exn
     1.9    val global_attribute: theory -> Args.src -> theory attribute
    1.10    val local_attribute: theory -> Args.src -> Proof.context attribute
    1.11 @@ -58,19 +59,23 @@
    1.12        attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
    1.13          error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
    1.14  
    1.15 -  fun print _ ({space, attrs}) =
    1.16 +  fun print_atts verbose ({space, attrs}) =
    1.17      let
    1.18        fun prt_attr (name, ((_, comment), _)) = Pretty.block
    1.19          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.20      in
    1.21 -      Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
    1.22 +      if not verbose then ()
    1.23 +      else Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
    1.24        Pretty.writeln (Pretty.big_list "attributes:"
    1.25          (map prt_attr (NameSpace.cond_extern_table space attrs)))
    1.26      end;
    1.27 +
    1.28 +   fun print _ = print_atts true;
    1.29  end;
    1.30  
    1.31  structure AttributesData = TheoryDataFun(AttributesDataArgs);
    1.32  val print_attributes = AttributesData.print;
    1.33 +val help_attributes = AttributesDataArgs.print_atts false o AttributesData.get;
    1.34  
    1.35  
    1.36  (* get global / local attributes *)
     2.1 --- a/src/Pure/Isar/method.ML	Thu Aug 26 19:01:22 1999 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 26 19:01:58 1999 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4  signature METHOD =
     2.5  sig
     2.6    include BASIC_METHOD
     2.7 +  val help_methods: theory -> unit
     2.8    val multi_resolve: thm list -> thm -> thm Seq.seq
     2.9    val FINISHED: tactic -> tactic
    2.10    val METHOD: (thm list -> tactic) -> Proof.method
    2.11 @@ -174,19 +175,23 @@
    2.12        meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
    2.13          error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
    2.14  
    2.15 -  fun print _ {space, meths} =
    2.16 +  fun print_meths verbose {space, meths} =
    2.17      let
    2.18        fun prt_meth (name, ((_, comment), _)) = Pretty.block
    2.19          [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    2.20      in
    2.21 -      Pretty.writeln (Display.pretty_name_space ("method name space", space));
    2.22 +      if not verbose then ()
    2.23 +      else Pretty.writeln (Display.pretty_name_space ("method name space", space));
    2.24        Pretty.writeln (Pretty.big_list "methods:"
    2.25          (map prt_meth (NameSpace.cond_extern_table space meths)))
    2.26      end;
    2.27 +
    2.28 +  fun print _ = print_meths true;
    2.29  end;
    2.30  
    2.31  structure MethodsData = TheoryDataFun(MethodsDataArgs);
    2.32  val print_methods = MethodsData.print;
    2.33 +val help_methods = MethodsDataArgs.print_meths false o MethodsData.get;
    2.34  
    2.35  
    2.36  (* get methods *)
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 26 19:01:22 1999 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 26 19:01:58 1999 +0200
     3.3 @@ -46,6 +46,7 @@
     3.4    val dest_keywords: unit -> string list
     3.5    val dest_parsers: unit -> (string * string * string * bool) list
     3.6    val print_outer_syntax: unit -> unit
     3.7 +  val print_help: Toplevel.transition -> Toplevel.transition
     3.8    val add_keywords: string list -> unit
     3.9    val add_parsers: parser list -> unit
    3.10    val theory_header: token list -> (string * string list * (string * bool) list) * token list
    3.11 @@ -191,6 +192,13 @@
    3.12        (map pretty_cmd int_cmds))
    3.13    end;
    3.14  
    3.15 +val print_help =
    3.16 +  Toplevel.imperative print_outer_syntax o
    3.17 +  Toplevel.keep (fn state =>
    3.18 +    (print_outer_syntax ();
    3.19 +      Method.help_methods (Toplevel.theory_of state);
    3.20 +      Attrib.help_attributes (Toplevel.theory_of state)));
    3.21 +
    3.22  
    3.23  
    3.24  (** read theory **)