dignostic commands: comment;

--- 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;

--- 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));