# HG changeset patch
# User wenzelm
# Date 1390422830 -3600
# Node ID 7df949045dc5436a3bdc9dd730cb490a67408514
# Parent  c0532866188357baffa3731b70a9ba375f268989
clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;

diff -r c05328661883 -r 7df949045dc5 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 17:22:26 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 21:33:50 2014 +0100
@@ -158,12 +158,15 @@
   |> filter (fn (_, tok) => Token.is_proper tok)
   |> clean;
 
-fun find_file toks =
-  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
-    if Token.is_name tok then
-      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
-        handle ERROR msg => error (msg ^ Token.pos_of tok)
-    else NONE);
+fun find_file ((_, tok) :: toks) =
+      if Token.is_command tok then
+        toks |> get_first (fn (i, tok) =>
+          if Token.is_name tok then
+            SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
+              handle ERROR msg => error (msg ^ Token.pos_of tok)
+          else NONE)
+      else NONE
+  | find_file [] = NONE;
 
 in
 
@@ -171,7 +174,7 @@
   (case span of
     Span (Command (cmd, pos), toks) =>
       if Keyword.is_theory_load cmd then
-        (case find_file toks of
+        (case find_file (clean_tokens toks) of
           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
         | SOME (i, path) =>
             let
diff -r c05328661883 -r 7df949045dc5 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 17:22:26 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 21:33:50 2014 +0100
@@ -235,8 +235,10 @@
         case t :: ts => t :: clean(ts)
         case Nil => Nil
       }
-    val clean_tokens = clean(tokens.filter(_.is_proper))
-    clean_tokens.reverse.find(_.is_name).map(_.content)
+    clean(tokens.filter(_.is_proper)) match {
+      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
+      case _ => None
+    }
   }
 
   def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =