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