1.1 --- a/src/Pure/General/position.ML	Wed Dec 16 16:25:55 2020 +0100
     1.2 +++ b/src/Pure/General/position.ML	Thu Dec 17 09:10:30 2020 +0100
     1.3 @@ -222,6 +222,7 @@
     1.4  fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
     1.5  fun report_text pos markup txt =
     1.6    ((** )@{print} {a = "### Position.report_text"};( *..NOT yet available*)
     1.7 +    writeln "### Position.report_text";
     1.8      Output.report [reported_text pos markup txt]);
     1.9  fun report pos markup = report_text pos markup "";
    1.10