equal
deleted
inserted
replaced
35 (for { |
35 (for { |
36 thy <- used_theories.iterator |
36 thy <- used_theories.iterator |
37 if theories.isEmpty || theories.contains(thy) |
37 if theories.isEmpty || theories.contains(thy) |
38 command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator |
38 command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator |
39 snapshot = Document.State.init.snippet(command) |
39 snapshot = Document.State.init.snippet(command) |
40 rendering = new Rendering(snapshot, options, session) |
40 (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator |
41 Text.Info(_, Protocol.ML_Profiling(report)) <- |
|
42 rendering.text_messages(Text.Range.full).iterator |
|
43 } yield if (clean_name) report.clean_name else report).toList |
41 } yield if (clean_name) report.clean_name else report).toList |
44 |
42 |
45 for (report <- ML_Profiling.account(reports)) progress.echo(report.print) |
43 for (report <- ML_Profiling.account(reports)) progress.echo(report.print) |
46 } |
44 } |
47 }) |
45 }) |