diff options
author | Nadrieril | 2019-08-03 22:55:51 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-06 21:40:24 +0200 |
commit | cc03ada4e713f145f2eb1bbf0f131a4c5746cf74 (patch) | |
tree | 6c4d1a59e3cfd621154b997ffe742768dc34c701 /dhall_generated_parser | |
parent | 8ec422f2319360f986950fcb9aae4bcf65a9c1e2 (diff) |
Inline headers
Diffstat (limited to '')
-rw-r--r-- | dhall_generated_parser/build.rs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dhall_generated_parser/build.rs b/dhall_generated_parser/build.rs index eab48bf..744cb3d 100644 --- a/dhall_generated_parser/build.rs +++ b/dhall_generated_parser/build.rs @@ -26,6 +26,7 @@ fn main() -> std::io::Result<()> { rules.get_mut(&line[2..]).map(|x| x.silent = true); } } + rules.remove("http"); rules.remove("simple_label"); rules.remove("nonreserved_label"); @@ -41,6 +42,17 @@ fn main() -> std::io::Result<()> { | !keyword ~ simple_label_first_char ~ simple_label_next_char* }}" )?; + // TODO: this is a cheat; actually implement inline headers instead + writeln!( + &mut file, + "http = {{ + http_raw + ~ (whsp + ~ using + ~ whsp1 + ~ (import_hashed | ^\"(\" ~ whsp ~ import_hashed ~ whsp ~ ^\")\"))? + }}" + )?; writeln!( &mut file, "nonreserved_label = _{{ |