# HG changeset patch
# User wenzelm
# Date 1606669040 -3600
# Node ID 98ecb951d911b2c665563beef06439b0e64567dc
# Parent  15a8de807f21b12fb53356e80cd1a18bad71c0c5
more completion;

diff -r 15a8de807f21 -r 98ecb951d911 src/Pure/PIDE/markup.scala
--- 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 */
 
diff -r 15a8de807f21 -r 98ecb951d911 src/Pure/Thy/thy_header.scala
--- 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