explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

--- a/src/Pure/Concurrent/future.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -61,7 +61,7 @@
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
   val shutdown: unit -> unit
-  val report: (unit -> 'a) -> 'a
+  val status: (unit -> 'a) -> 'a
 end;
 
 structure Future: FUTURE =
@@ -532,9 +532,9 @@
   else ();
 
 
-(* report markup *)
+(* status markup *)
 
-fun report e =
+fun status e =
   let
     val _ = Output.status (Markup.markup Markup.forked "");
     val x = e ();  (*sic -- report "joined" only for success*)

--- a/src/Pure/General/markup.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/General/markup.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -196,6 +196,7 @@
 
   val INIT = "init"
   val STATUS = "status"
+  val REPORT = "report"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"

--- a/src/Pure/General/output.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/General/output.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -39,9 +39,11 @@
   val debug_fn: (output -> unit) Unsynchronized.ref
   val prompt_fn: (output -> unit) Unsynchronized.ref
   val status_fn: (output -> unit) Unsynchronized.ref
+  val report_fn: (output -> unit) Unsynchronized.ref
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
+  val report: string -> unit
   val debugging: bool Unsynchronized.ref
   val no_warnings_CRITICAL: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
@@ -98,6 +100,7 @@
 val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
 val prompt_fn = Unsynchronized.ref std_output;
 val status_fn = Unsynchronized.ref (fn _: string => ());
+val report_fn = Unsynchronized.ref (fn _: string => ());
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
@@ -106,6 +109,7 @@
 fun error_msg s = ! error_fn (output s);
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
+fun report s = ! report_fn (output s);
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 

--- a/src/Pure/General/position.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/General/position.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -127,7 +127,7 @@
 
 fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
-  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
 
 fun report markup pos = report_text markup pos "";
 

--- a/src/Pure/Isar/isar_document.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -233,7 +233,7 @@
     val _ = define_state state_id' state';
   in (state_id', (id, state_id') :: updates) end;
 
-fun report_updates updates =
+fun updates_status updates =
   implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   |> Markup.markup Markup.assign
   |> Output.status;
@@ -262,7 +262,7 @@
           |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
       val _ = define_document new_id new_document';
-      val _ = report_updates (flat updatess);
+      val _ = updates_status (flat updatess);
       val _ = execute new_document';
     in () end);
 

--- a/src/Pure/Isar/isar_document.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -9,7 +9,7 @@
 
 object Isar_Document
 {
-  /* reports */
+  /* protocol messages */
 
   object Assign {
     def unapply(msg: XML.Tree): Option[List[XML.Tree]] =

--- a/src/Pure/Isar/keyword.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/keyword.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -44,8 +44,8 @@
   val dest_commands: unit -> string list
   val command_keyword: string -> T option
   val command_tags: string -> string list
-  val keyword_status_reportN: string
-  val report: unit -> unit
+  val keyword_statusN: string
+  val status: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
   val is_diag: string -> bool
@@ -146,27 +146,27 @@
 fun command_tags name = these (Option.map tags_of (command_keyword name));
 
 
-(* reports *)
+(* status *)
 
-val keyword_status_reportN = "keyword_status_report";
+val keyword_statusN = "keyword_status";
 
-fun report_message s =
-  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
+fun status_message s =
+  (if print_mode_active keyword_statusN then Output.status else writeln) s;
 
-fun report_keyword name =
-  report_message (Markup.markup (Markup.keyword_decl name)
+fun keyword_status name =
+  status_message (Markup.markup (Markup.keyword_decl name)
     ("Outer syntax keyword: " ^ quote name));
 
-fun report_command (name, kind) =
-  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
+fun command_status (name, kind) =
+  status_message (Markup.markup (Markup.command_decl name (kind_of kind))
     ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
 
-fun report () =
+fun status () =
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in
-    List.app report_keyword keywords;
-    List.app report_command commands
+    List.app keyword_status keywords;
+    List.app command_status commands
   end;
 
 
@@ -174,12 +174,12 @@
 
 fun keyword name =
  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  report_keyword name);
+  keyword_status name);
 
 fun command name kind =
  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
-  report_command (name, kind));
+  command_status (name, kind));
 
 
 (* command categories *)

--- a/src/Pure/Isar/keyword.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/keyword.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -50,7 +50,7 @@
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 
 
-  /* reports */
+  /* protocol messages */
 
   object Keyword_Decl {
     def unapply(msg: XML.Tree): Option[String] =

--- a/src/Pure/Isar/outer_syntax.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -277,7 +277,7 @@
 
     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
-    val _ = List.app Thy_Syntax.report_span spans;
+    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
     val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
       |> Par_List.map (prepare_unit commands init) |> flat;
 

--- a/src/Pure/Isar/toplevel.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -571,7 +571,7 @@
   if print then
     ignore
       (Future.fork (fn () =>
-          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
+          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
   else ();
 
 fun error_msg tr exn_info =

--- a/src/Pure/PIDE/state.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Accumulating results from prover.
+Accumulated results from prover.
 */
 
 package isabelle
@@ -84,6 +84,12 @@
             case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
             case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
             case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
+            case _ => System.err.println("Ignored status message: " + elem); state
+          })
+
+      case XML.Elem(Markup(Markup.REPORT, _), elems) =>
+        (this /: elems)((state, elem) =>
+          elem match {
             case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
               atts match {
                 case Position.Range(begin, end) =>
@@ -112,9 +118,7 @@
                   }
                 case _ => state
               }
-            case _ =>
-              System.err.println("Ignored status report: " + elem)
-              state
+            case _ => System.err.println("Ignored report message: " + elem); state
           })
       case _ => add_result(message)
     }

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -78,6 +78,7 @@
 fun setup_messages () =
  (Output.writeln_fn := message "" "" "";
   Output.status_fn := (fn _ => ());
+  Output.report_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") "+++ ";

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -161,6 +161,7 @@
 fun setup_messages () =
  (Output.writeln_fn := (fn s => normalmsg Message s);
   Output.status_fn := (fn _ => ());
+  Output.report_fn := (fn _ => ());
   Output.priority_fn := (fn s => normalmsg Status s);
   Output.tracing_fn := (fn s => normalmsg Tracing s);
   Output.warning_fn := (fn s => errormsg Message Warning s);

--- a/src/Pure/System/isabelle_process.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -72,11 +72,12 @@
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   in
     Output.status_fn   := standard_message out_stream "B";
-    Output.writeln_fn  := standard_message out_stream "C";
-    Output.tracing_fn  := standard_message out_stream "D";
-    Output.warning_fn  := standard_message out_stream "E";
-    Output.error_fn    := standard_message out_stream "F";
-    Output.debug_fn    := standard_message out_stream "G";
+    Output.report_fn   := standard_message out_stream "C";
+    Output.writeln_fn  := standard_message out_stream "D";
+    Output.tracing_fn  := standard_message out_stream "E";
+    Output.warning_fn  := standard_message out_stream "F";
+    Output.error_fn    := standard_message out_stream "G";
+    Output.debug_fn    := standard_message out_stream "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     out_stream
@@ -89,10 +90,10 @@
 
 fun init out =
  (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
+    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
   setup_channels out |> init_message;
   quick_and_dirty := true;  (* FIXME !? *)
-  Keyword.report ();
+  Keyword.status ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 

--- a/src/Pure/System/isabelle_process.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -24,11 +24,12 @@
     val markup = Map(
       ('A' : Int) -> Markup.INIT,
       ('B' : Int) -> Markup.STATUS,
-      ('C' : Int) -> Markup.WRITELN,
-      ('D' : Int) -> Markup.TRACING,
-      ('E' : Int) -> Markup.WARNING,
-      ('F' : Int) -> Markup.ERROR,
-      ('G' : Int) -> Markup.DEBUG)
+      ('C' : Int) -> Markup.REPORT,
+      ('D' : Int) -> Markup.WRITELN,
+      ('E' : Int) -> Markup.TRACING,
+      ('F' : Int) -> Markup.WARNING,
+      ('G' : Int) -> Markup.ERROR,
+      ('H' : Int) -> Markup.DEBUG)
     def is_raw(kind: String) =
       kind == Markup.STDOUT
     def is_control(kind: String) =
@@ -53,12 +54,13 @@
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
     def is_status = kind == Markup.STATUS
+    def is_report = kind == Markup.REPORT
     def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
 
     override def toString: String =
     {
       val res =
-        if (is_status) message.body.map(_.toString).mkString
+        if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"

--- a/src/Pure/goal.ML	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/goal.ML	Sun Aug 08 19:36:31 2010 +0200
@@ -103,7 +103,7 @@
 
 (* parallel proofs *)
 
-fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
+fun fork e = Future.fork_pri ~1 (fn () => Future.status e);
 
 val parallel_proofs = Unsynchronized.ref 1;