more accurate syntax, following Sessions.parse_roots in Scala;

--- a/src/Pure/Pure.thy	Sun Dec 06 16:27:37 2020 +0100
+++ b/src/Pure/Pure.thy	Sun Dec 06 20:49:44 2020 +0100
@@ -137,8 +137,12 @@
                   val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
                   val pos = Position.range_position (pos1, pos2);
                   val _ =
-                    ignore (Resources.check_dir ctxt (SOME dir) (line, pos))
-                      handle ERROR msg => Output.error_message msg;
+                    if line = "" then ()
+                    else if String.isPrefix "#" line then
+                      Context_Position.report ctxt pos Markup.comment
+                    else
+                      (ignore (Resources.check_dir ctxt (SOME dir) (line, pos))
+                        handle ERROR msg => Output.error_message msg);
                 in pos2 |> Position.advance "\n" end);
           in thy' end)));