78 |
78 |
79 /* header */ |
79 /* header */ |
80 |
80 |
81 val header: Parser[Thy_Header] = |
81 val header: Parser[Thy_Header] = |
82 { |
82 { |
83 val file_name = atom("file name", _.is_name) |
|
84 |
|
85 val opt_files = |
83 val opt_files = |
86 $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
84 $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | |
87 success(Nil) |
85 success(Nil) |
|
86 |
88 val keyword_spec = |
87 val keyword_spec = |
89 atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ |
88 atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ |
90 { case x ~ y ~ z => ((x, y), z) } |
89 { case x ~ y ~ z => ((x, y), z) } |
91 |
90 |
92 val keyword_decl = |
91 val keyword_decl = |
93 rep1(string) ~ |
92 rep1(string) ~ |
94 opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ |
93 opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ |
95 opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^ |
94 opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^ |
96 { case xs ~ y ~ z => xs.map((_, y, z)) } |
95 { case xs ~ y ~ z => xs.map((_, y, z)) } |
|
96 |
97 val keyword_decls = |
97 val keyword_decls = |
98 keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
98 keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ |
99 { case xs ~ yss => (xs :: yss).flatten } |
99 { case xs ~ yss => (xs :: yss).flatten } |
100 |
100 |
101 val file = |
|
102 $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
|
103 file_name ^^ (x => (x, true)) |
|
104 |
|
105 val args = |
101 val args = |
106 theory_name ~ |
102 position(theory_name) ~ |
107 (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^ |
103 (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^ |
108 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
104 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
109 (opt($$$(KEYWORDS) ~! keyword_decls) ^^ |
105 (opt($$$(KEYWORDS) ~! keyword_decls) ^^ |
110 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
106 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
111 $$$(BEGIN) ^^ |
107 $$$(BEGIN) ^^ |
112 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
108 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
154 read(new CharSequenceReader(source)) |
150 read(new CharSequenceReader(source)) |
155 } |
151 } |
156 |
152 |
157 |
153 |
158 sealed case class Thy_Header( |
154 sealed case class Thy_Header( |
159 name: String, |
155 name: (String, Position.T), |
160 imports: List[String], |
156 imports: List[(String, Position.T)], |
161 keywords: Thy_Header.Keywords) |
157 keywords: Thy_Header.Keywords) |
162 { |
158 { |
163 def map(f: String => String): Thy_Header = |
|
164 Thy_Header(f(name), imports.map(f), keywords) |
|
165 |
|
166 def decode_symbols: Thy_Header = |
159 def decode_symbols: Thy_Header = |
167 { |
160 { |
168 val f = Symbol.decode _ |
161 val f = Symbol.decode _ |
169 Thy_Header(f(name), imports.map(f), |
162 Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }), |
170 keywords.map({ case (a, b, c) => |
163 keywords.map({ case (a, b, c) => |
171 (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) })) |
164 (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) })) |
172 } |
165 } |
173 } |
166 } |
174 |
|