# HG changeset patch
# User wenzelm
# Date 1623188046 -7200
# Node ID 0e6a5a6cc767246010bfa10a062c19817d25854f
# Parent  f72335f6a9edf6c7f5b3a1d29910b6a43f35defa
prefer less intrusive tracing message;

diff -r f72335f6a9ed -r 0e6a5a6cc767 src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML	Tue Jun 08 23:23:59 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Tue Jun 08 23:34:06 2021 +0200
@@ -34,7 +34,7 @@
           val xml =
             XML.Elem (Markup.ML_profiling kind,
               XML.Text (title ^ "\n") :: body @ [XML.Text (print_entry total "TOTAL")]);
-        in warning (YXML.string_of xml) end)) mode f x;
+        in tracing (YXML.string_of xml) end)) mode f x;
 
 fun profile_time f =
   profile PolyML.Profiling.ProfileTime "time" "time profile:" f;
diff -r f72335f6a9ed -r 0e6a5a6cc767 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Jun 08 23:23:59 2021 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Jun 08 23:34:06 2021 +0200
@@ -216,7 +216,7 @@
   {
     def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] =
       msg match {
-        case XML.Elem(_, List(tree)) if is_warning(msg) =>
+        case XML.Elem(_, List(tree)) if is_tracing(msg) =>
           Markup.ML_Profiling.unapply_report(tree)
         case _ => None
       }
diff -r f72335f6a9ed -r 0e6a5a6cc767 src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Tue Jun 08 23:23:59 2021 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Tue Jun 08 23:34:06 2021 +0200
@@ -37,9 +37,7 @@
               if theories.isEmpty || theories.contains(thy)
               command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator
               snapshot = Document.State.init.snippet(command)
-              rendering = new Rendering(snapshot, options, session)
-              Text.Info(_, Protocol.ML_Profiling(report)) <-
-                rendering.text_messages(Text.Range.full).iterator
+              (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList
 
           for (report <- ML_Profiling.account(reports)) progress.echo(report.print)