56 def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name) |
56 def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name) |
57 def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1) |
57 def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1) |
58 |
58 |
59 def thy_load(span: List[Token]): Option[List[String]] = |
59 def thy_load(span: List[Token]): Option[List[String]] = |
60 keywords.get(Command.name(span)) match { |
60 keywords.get(Command.name(span)) match { |
61 case Some((Keyword.THY_LOAD, files)) => Some(files) |
61 case Some((Keyword.THY_LOAD, exts)) => Some(exts) |
62 case _ => None |
62 case _ => None |
63 } |
63 } |
64 |
64 |
65 def thy_load_commands: List[(String, List[String])] = |
65 val thy_load_commands: List[(String, List[String])] = |
66 (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList |
66 (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList |
67 |
67 |
68 def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax = |
68 def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax = |
69 { |
69 { |
70 val keywords1 = keywords + (name -> kind) |
70 val keywords1 = keywords + (name -> kind) |