src/Pure/Thy/thy_header.scala
changeset 72782 98ecb951d911
parent 72779 1cc74982d038
child 72853 d0038b553e0e
equal deleted inserted replaced
72781:15a8de807f21 72782:98ecb951d911
   257       if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) {
   257       if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) {
   258         error("Illegal load command specification for kind: " + quote(spec.kind) +
   258         error("Illegal load command specification for kind: " + quote(spec.kind) +
   259           Position.here(spec.kind_pos))
   259           Position.here(spec.kind_pos))
   260       }
   260       }
   261       if (!Command_Span.load_commands.exists(_.name == spec.load_command)) {
   261       if (!Command_Span.load_commands.exists(_.name == spec.load_command)) {
       
   262         val completion =
       
   263           for {
       
   264             load_command <- Command_Span.load_commands
       
   265             name = load_command.name
       
   266             if name.startsWith(spec.load_command)
       
   267           } yield (name, (Markup.LOAD_COMMAND, name))
   262         error("Unknown load command specification: " + quote(spec.load_command) +
   268         error("Unknown load command specification: " + quote(spec.load_command) +
   263           Position.here(spec.load_command_pos))
   269           Position.here(spec.load_command_pos) +
       
   270           Completion.report_names(spec.load_command_pos, completion))
   264       }
   271       }
   265     }
   272     }
   266     this
   273     this
   267   }
   274   }
   268 }
   275 }