# HG changeset patch
# User wenzelm
# Date 1606602536 -3600
# Node ID f34f5c057c9ee1c5bcf292323734089429674e94
# Parent  722c0d02ffabc74a689fdd987641bfedc6e5ed58
clarified parsing vs. semantic errors;

diff -r 722c0d02ffab -r f34f5c057c9e src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Sat Nov 28 22:20:48 2020 +0100
+++ b/src/Pure/Isar/keyword.scala	Sat Nov 28 23:28:56 2020 +0100
@@ -108,7 +108,9 @@
 
   sealed case class Spec(
     kind: String = "",
+    kind_pos: Position.T = Position.none,
     load_command: String = "",
+    load_command_pos: Position.T = Position.none,
     tags: List[String] = Nil)
   {
     override def toString: String =
diff -r 722c0d02ffab -r f34f5c057c9e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Nov 28 22:20:48 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Nov 28 23:28:56 2020 +0100
@@ -424,21 +424,18 @@
           }
           catch { case _: Throwable => List.fill(imports_pos.length)("") }
 
-        val errs1 =
+        val errors =
           for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
           yield {
             val completion =
               if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
-            "Bad theory import " +
-              Markup.Path(import_name.node).markup(quote(import_name.toString)) +
-              Position.here(pos) + Completion.report_theories(pos, completion)
+            val msg =
+              "Bad theory import " +
+                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
+                Position.here(pos) + Completion.report_theories(pos, completion)
+            Exn.Exn[Command.Blob](ERROR(msg))
           }
-        val errs2 =
-          for {
-            (_, spec) <- header.keywords
-            if !Command_Span.load_commands.exists(_.name == spec.load_command)
-          } yield { "Unknown load command specification: " + quote(spec.load_command) }
-      ((errs1 ::: errs2).map(msg => Exn.Exn[Command.Blob](ERROR(msg))), -1)
+        (errors, -1)
 
       // auxiliary files
       case _ =>
diff -r 722c0d02ffab -r f34f5c057c9e src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Nov 28 22:20:48 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Nov 28 23:28:56 2020 +0100
@@ -221,7 +221,7 @@
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader, start, strict)
+        val header = Thy_Header.read(reader, start, strict).check_keywords
 
         val base_name = node_name.theory_base_name
         if (Long_Name.is_qualified(header.name)) {
diff -r 722c0d02ffab -r f34f5c057c9e src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat Nov 28 22:20:48 2020 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Nov 28 23:28:56 2020 +0100
@@ -132,14 +132,12 @@
   if name = Context.PureN then Scan.succeed []
   else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name);
 
-fun loaded_files kind =
-  if kind = Keyword.thy_load then
-    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []
-  else Scan.succeed [];
+val load_command =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
 
 val keyword_spec =
   Parse.group (fn () => "outer syntax keyword specification")
-    ((Parse.name :-- loaded_files >> #1) -- Document_Source.old_tags);
+    ((Parse.name --| load_command) -- Document_Source.old_tags);
 
 val keyword_decl =
   Scan.repeat1 Parse.string_position --
diff -r 722c0d02ffab -r f34f5c057c9e src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Nov 28 22:20:48 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Nov 28 23:28:56 2020 +0100
@@ -129,15 +129,17 @@
   {
     val header: Parser[Thy_Header] =
     {
-      def load_command =
-        ($$$("(") ~! (name <~ $$$(")")) ^^ { case _ ~ x => x }) | success("")
+      val load_command =
+        ($$$("(") ~! (position(name) <~ $$$(")")) ^^ { case _ ~ x => x }) |
+          success(("", Position.none))
 
-      def load_command_spec(kind: String) =
-        (if (kind == Keyword.THY_LOAD) load_command else success("")) ^^ (x => (kind, x))
-
+      val keyword_kind = atom("outer syntax keyword specification", _.is_name)
       val keyword_spec =
-        (atom("outer syntax keyword specification", _.is_name) >> load_command_spec) ~ tags ^^
-        { case (x, y) ~ z => Keyword.Spec(kind = x, load_command = y, tags = z) }
+        position(keyword_kind) ~ load_command ~ tags ^^
+          { case (a, b) ~ c ~ d =>
+              Keyword.Spec(kind = a, kind_pos = b,
+                load_command = c._1, load_command_pos = c._2, tags = d)
+          }
 
       val keyword_decl =
         rep1(string) ~
@@ -238,4 +240,19 @@
       imports_pos.map({ case (a, b) => (f(a), b) }),
       keywords.map({ case (a, spec) => (f(a), spec.map(f)) }),
       abbrevs.map({ case (a, b) => (f(a), f(b)) }))
+
+  def check_keywords: Thy_Header =
+  {
+    for ((_, spec) <- keywords) {
+      if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) {
+        error("Illegal load command specification for kind: " + quote(spec.kind) +
+          Position.here(spec.kind_pos))
+      }
+      if (!Command_Span.load_commands.exists(_.name == spec.load_command)) {
+        error("Unknown load command specification: " + quote(spec.load_command) +
+          Position.here(spec.load_command_pos))
+      }
+    }
+    this
+  }
 }