49 val theory_name = atom("theory name", _.is_name) |
49 val theory_name = atom("theory name", _.is_name) |
50 |
50 |
51 val keyword_kind = |
51 val keyword_kind = |
52 atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } |
52 atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } |
53 val keyword_decl = |
53 val keyword_decl = |
54 name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^ |
54 rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^ |
55 { case x ~ y => (x, y) } |
55 { case xs ~ y => xs.map((_, y)) } |
56 val keywords = |
56 val keyword_decls = |
57 keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
57 keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
58 { case x ~ ys => x :: ys } |
58 { case xs ~ yss => (xs :: yss).flatten } |
59 |
59 |
60 val file = |
60 val file = |
61 keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
61 keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
62 file_name ^^ (x => (x, true)) |
62 file_name ^^ (x => (x, true)) |
63 |
63 |
64 val args = |
64 val args = |
65 theory_name ~ |
65 theory_name ~ |
66 (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~ |
66 (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~ |
67 (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
67 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
68 (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
68 (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
69 keyword(BEGIN) ^^ |
69 keyword(BEGIN) ^^ |
70 { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } |
70 { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } |
71 |
71 |
72 (keyword(HEADER) ~ tags) ~! |
72 (keyword(HEADER) ~ tags) ~! |