diff options
| author | Pierre-Marie Pédrot | 2018-09-26 16:41:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-01 20:00:47 +0200 |
| commit | 6c5356f7a77600a4cd35a07897f84bb4fa71b8ad (patch) | |
| tree | bf30044c382fabd52be52f19e1008cb39b07f45f /coqpp | |
| parent | e54df5786d93a1d38b730dfc95a11fea996cff84 (diff) | |
Store locations of OCaml quotations in coqpp.
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_ast.mli | 2 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 15 |
2 files changed, 11 insertions, 6 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 181c43615b..956a916792 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -11,7 +11,7 @@ type loc = { loc_end : Lexing.position; } -type code = { code : string } +type code = { code : string; loc : loc; } type user_symbol = | Ulist1 of user_symbol diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index bfa4e2b57b..81a53e887b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -29,6 +29,7 @@ let newline lexbuf = let num_comments = ref 0 let num_braces = ref 0 +let ocaml_start_pos = ref Lexing.dummy_pos let mode () = if !num_braces = 0 then Extend else OCaml @@ -57,10 +58,10 @@ let end_comment lexbuf = else None -let start_ocaml _ = +let start_ocaml lexbuf = let () = match mode () with | OCaml -> Buffer.add_string ocaml_buf "{" - | Extend -> () + | Extend -> ocaml_start_pos := lexeme_start_p lexbuf in incr num_braces @@ -70,7 +71,11 @@ let end_ocaml lexbuf = else if !num_braces = 0 then let s = Buffer.contents ocaml_buf in let () = Buffer.reset ocaml_buf in - Some (CODE { Coqpp_ast.code = s }) + let loc = { + Coqpp_ast.loc_start = !ocaml_start_pos; + Coqpp_ast.loc_end = lexeme_end_p lexbuf + } in + Some (CODE { Coqpp_ast.code = s; loc }) else let () = Buffer.add_string ocaml_buf "}" in None @@ -87,7 +92,7 @@ let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "GRAMMAR" { GRAMMAR } | "VERNAC" { VERNAC } | "TACTIC" { TACTIC } @@ -127,7 +132,7 @@ rule extend = parse | eof { EOF } and ocaml = parse -| "{" { start_ocaml (); ocaml lexbuf } +| "{" { start_ocaml lexbuf; ocaml lexbuf } | "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf } | '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf } | '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf } |