more completion;

--- a/src/Pure/PIDE/markup.scala	Sun Nov 29 17:54:50 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Nov 29 17:57:20 2020 +0100
@@ -380,6 +380,8 @@
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
+  val LOAD_COMMAND = "load_command"
+
 
   /* comments */
 

--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 17:54:50 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 17:57:20 2020 +0100
@@ -259,8 +259,15 @@
           Position.here(spec.kind_pos))
       }
       if (!Command_Span.load_commands.exists(_.name == spec.load_command)) {
+        val completion =
+          for {
+            load_command <- Command_Span.load_commands
+            name = load_command.name
+            if name.startsWith(spec.load_command)
+          } yield (name, (Markup.LOAD_COMMAND, name))
         error("Unknown load command specification: " + quote(spec.load_command) +
-          Position.here(spec.load_command_pos))
+          Position.here(spec.load_command_pos) +
+          Completion.report_names(spec.load_command_pos, completion))
       }
     }
     this