# HG changeset patch # User wenzelm # Date 975968243 -3600 # Node ID 74e542a299f04d9f7c554411309b2542aff84251 # Parent 930ac2bfa6379cc65878b85e22e79fdc5bb7d0c8 dignostic commands: comment; diff -r 930ac2bfa637 -r 74e542a299f0 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Dec 04 23:16:25 2000 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Mon Dec 04 23:17:23 2000 +0100 @@ -55,11 +55,14 @@ val print_binds: Toplevel.transition -> Toplevel.transition val print_lthms: Toplevel.transition -> Toplevel.transition val print_cases: Toplevel.transition -> Toplevel.transition - val print_thms: string list * (string * Args.src list) list + val print_thms: (string list * (string * Args.src list) list) * Comment.text + -> Toplevel.transition -> Toplevel.transition + val print_prop: (string list * string) * Comment.text -> Toplevel.transition -> Toplevel.transition - val print_prop: string list * string -> Toplevel.transition -> Toplevel.transition - val print_term: string list * string -> Toplevel.transition -> Toplevel.transition - val print_type: string list * string -> Toplevel.transition -> Toplevel.transition + val print_term: (string list * string) * Comment.text + -> Toplevel.transition -> Toplevel.transition + val print_type: (string list * string) * Comment.text + -> Toplevel.transition -> Toplevel.transition end; structure IsarCmd: ISAR_CMD = @@ -245,10 +248,10 @@ fun print_item string_of (x, y) = Toplevel.keep (fn state => writeln (string_of (Toplevel.enter_forward_proof state) x y)); -val print_thms = print_item string_of_thms; -val print_prop = print_item string_of_prop; -val print_term = print_item string_of_term; -val print_type = print_item string_of_type; +val print_thms = print_item string_of_thms o Comment.ignore; +val print_prop = print_item string_of_prop o Comment.ignore; +val print_term = print_item string_of_term o Comment.ignore; +val print_type = print_item string_of_type o Comment.ignore; end; diff -r 930ac2bfa637 -r 74e542a299f0 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Dec 04 23:16:25 2000 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Dec 04 23:17:23 2000 +0100 @@ -560,19 +560,19 @@ val print_thmsP = OuterSyntax.improper_command "thm" "print theorems" K.diag - (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); + (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_thms)); val print_propP = OuterSyntax.improper_command "prop" "read and print proposition" K.diag - (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); + (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prop)); val print_termP = OuterSyntax.improper_command "term" "read and print term" K.diag - (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); + (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_term)); val print_typeP = OuterSyntax.improper_command "typ" "read and print type" K.diag - (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); + (opt_modes -- P.typ -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_type));