equal
deleted
inserted
replaced
129 |
129 |
130 trait Parser extends Parse.Parser |
130 trait Parser extends Parse.Parser |
131 { |
131 { |
132 val header: Parser[Thy_Header] = |
132 val header: Parser[Thy_Header] = |
133 { |
133 { |
134 val opt_files = |
134 val loaded_files = |
135 $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
135 $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
136 success(Nil) |
136 success(Nil) |
137 |
137 |
138 val keyword_spec = |
138 val keyword_spec = |
139 atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ |
139 atom("outer syntax keyword specification", _.is_name) ~ loaded_files ~ tags ^^ |
140 { case x ~ y ~ z => Keyword.Spec(x, y, z) } |
140 { case x ~ y ~ z => Keyword.Spec(x, y, z) } |
141 |
141 |
142 val keyword_decl = |
142 val keyword_decl = |
143 rep1(string) ~ |
143 rep1(string) ~ |
144 opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ |
144 opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ |