suppress status output for traditional tty modes (including Proof General);
keyword report: explicitly issue message on writeln channel as well;
--- a/src/Pure/General/output.ML Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/General/output.ML Mon Mar 23 17:21:42 2009 +0100
@@ -101,7 +101,7 @@
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
val prompt_fn = ref std_output;
-val status_fn = ref (fn s => ! writeln_fn s);
+val status_fn = ref (fn _: string => ());
fun writeln s = ! writeln_fn (output s);
fun priority s = ! priority_fn (output s);
--- a/src/Pure/Isar/outer_keyword.ML Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML Mon Mar 23 17:21:42 2009 +0100
@@ -150,23 +150,25 @@
Pretty.mark (Markup.command_decl name (kind_of kind))
(Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
+fun status_writeln s = (Output.status s; writeln s);
+
fun report () =
let val (keywords, commands) = CRITICAL (fn () =>
(dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
in map report_keyword keywords @ map report_command commands end
- |> Pretty.chunks |> Pretty.string_of |> Output.status;
+ |> Pretty.chunks |> Pretty.string_of |> status_writeln;
(* augment tables *)
fun keyword name =
(change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
- Output.status (Pretty.string_of (report_keyword name)));
+ status_writeln (Pretty.string_of (report_keyword name)));
fun command name kind =
(change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
change_commands (Symtab.update (name, kind));
- Output.status (Pretty.string_of (report_command (name, kind))));
+ status_writeln (Pretty.string_of (report_command (name, kind))));
(* command categories *)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Mar 23 17:20:31 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Mar 23 17:21:42 2009 +0100
@@ -76,7 +76,7 @@
fun setup_messages () =
(Output.writeln_fn := message "" "" "";
- Output.status_fn := (fn s => ! Output.priority_fn s);
+ Output.status_fn := (fn _ => ());
Output.priority_fn := message (special "I") (special "J") "";
Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
Output.debug_fn := message (special "K") (special "L") "+++ ";