src/Pure/Isar/outer_syntax.scala

   override def toString: String = keywords.toString
 
 
   /* keywords */
 
-  def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
+  def + (name: String, kind: String = "", load_command: String = ""): Outer_Syntax =
     new Outer_Syntax(
-      keywords + (name, kind, exts), rev_abbrevs, language_context, has_tokens = true)
+      keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
       case (syntax, (name, spec)) =>
         syntax +
-          (Symbol.decode(name), spec.kind, spec.exts) +
-          (Symbol.encode(name), spec.kind, spec.exts)
+          (Symbol.decode(name), spec.kind, spec.load_command) +
+          (Symbol.encode(name), spec.kind, spec.load_command)
     }
 
 
   /* abbrevs */
 

     }
 
 
   /* load commands */
 
-  def load_command(name: String): Option[List[String]] =
+  def load_command(name: String): Option[String] =
     keywords.load_commands.get(name)
 
   def has_load_commands(text: String): Boolean =
     keywords.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })