equal
deleted
inserted
replaced
118 fun output () = |
118 fun output () = |
119 persistent_reports |
119 persistent_reports |
120 |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) |
120 |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) |
121 |> |
121 |> |
122 ((** )@{print} {a = "### ML_Compiler.output"};( *..NOT yet available 2 *) |
122 ((** )@{print} {a = "### ML_Compiler.output"};( *..NOT yet available 2 *) |
|
123 (**)writeln "### ML_Compiler.output";(**) |
123 Output.report); |
124 Output.report); |
124 val _ = |
125 val _ = |
125 if not (null persistent_reports) andalso redirect andalso Future.enabled () |
126 if not (null persistent_reports) andalso redirect andalso Future.enabled () |
126 then |
127 then |
127 Execution.print |
128 Execution.print |