# HG changeset patch
# User wenzelm
# Date 1607284184 -3600
# Node ID 27a7a54995112305acba3bde6f9c64d05ef659ee
# Parent  2c26c283f3ee2c7d322689c3e6b084342ba7076d
more accurate syntax, following Sessions.parse_roots in Scala;

diff -r 2c26c283f3ee -r 27a7a5499511 src/Pure/Pure.thy
--- 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)));