equal
deleted
inserted
replaced
65 keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
65 keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | |
66 file_name ^^ (x => (x, true)) |
66 file_name ^^ (x => (x, true)) |
67 |
67 |
68 val args = |
68 val args = |
69 theory_name ~ |
69 theory_name ~ |
70 (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
70 (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ |
71 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ |
71 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
|
72 (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ |
|
73 { case None => Nil case Some(_ ~ xs) => xs }) ~ |
72 keyword(BEGIN) ^^ |
74 keyword(BEGIN) ^^ |
73 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
75 { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } |
74 |
76 |
75 (keyword(HEADER) ~ tags) ~! |
77 (keyword(HEADER) ~ tags) ~! |
76 ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | |
78 ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ |
|
79 { case _ ~ x => x } | |
77 (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
80 (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } |
78 } |
81 } |
79 |
82 |
80 |
83 |
81 /* read -- lazy scanning */ |
84 /* read -- lazy scanning */ |
117 imports: List[String], |
120 imports: List[String], |
118 keywords: Thy_Header.Keywords) |
121 keywords: Thy_Header.Keywords) |
119 { |
122 { |
120 def map(f: String => String): Thy_Header = |
123 def map(f: String => String): Thy_Header = |
121 Thy_Header(f(name), imports.map(f), keywords) |
124 Thy_Header(f(name), imports.map(f), keywords) |
|
125 |
|
126 def decode_symbols: Thy_Header = |
|
127 { |
|
128 val f = Symbol.decode _ |
|
129 Thy_Header(f(name), imports.map(f), |
|
130 keywords.map({ case (a, b, c) => |
|
131 (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) })) |
|
132 } |
122 } |
133 } |
123 |
134 |