Commit bf7ca1d4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use Lexing.new_line whenever possible.

parent ffd11734
Pipeline #14175 failed with stage
in 2 minutes and 43 seconds
......@@ -45,11 +45,6 @@
fun s -> try Hashtbl.find h s with Not_found ->
raise (Lexing_error ("no such annotation '" ^ s ^ "'"))
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let string_buffer = Buffer.create 1024
let stack = ref [0] (* indentation stack *)
......@@ -77,7 +72,7 @@ let space = ' ' | '\t'
let comment = "#" [^'@''\n'] [^'\n']*
rule next_tokens = parse
| '\n' { newline lexbuf; update_stack (indentation lexbuf) }
| '\n' { new_line lexbuf; update_stack (indentation lexbuf) }
| (space | comment)+
{ next_tokens lexbuf }
| "\\" space* '\n' space* "#@"?
......@@ -120,7 +115,7 @@ rule next_tokens = parse
and indentation = parse
| (space | comment)* '\n'
(* skip empty lines *)
{ newline lexbuf; indentation lexbuf }
{ new_line lexbuf; indentation lexbuf }
| space* as s
{ String.length s }
......
......@@ -96,11 +96,6 @@
"type", TYPE;
]
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let comment_start_loc = ref Loc.dummy_position
let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb)
......@@ -126,7 +121,7 @@ let do_char = [' '-'!' '#'-'[' ']'-'~'] | '\\' ['\\' '"']
rule token = parse
| newline
{ newline lexbuf; token lexbuf }
{ new_line lexbuf; token lexbuf }
| space+
{ token lexbuf }
| lword as id
......@@ -222,7 +217,7 @@ and comment_block = parse
| "*/"
{ () }
| newline
{ newline lexbuf; comment_block lexbuf }
{ new_line lexbuf; comment_block lexbuf }
| eof
{ raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
| _
......@@ -230,7 +225,7 @@ and comment_block = parse
and comment_line = parse
| newline
{ newline lexbuf; () }
{ new_line lexbuf; () }
| eof
{ () }
| _
......
......@@ -72,7 +72,7 @@ let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%'
rule token = parse
| '\n'
{ Lexlib.newline lexbuf; token lexbuf }
{ new_line lexbuf; token lexbuf }
| space+
{ token lexbuf }
| "(*)"
......
......@@ -140,7 +140,7 @@ rule token = parse
| "[@" space* ([^ ' ' '\n' ']']+ (' '+ [^ ' ' '\n' ']']+)* as lbl) space* ']'
{ ATTRIBUTE lbl }
| '\n'
{ Lexlib.newline lexbuf; token lexbuf }
{ Lexing.new_line lexbuf; token lexbuf }
| space+
{ token lexbuf }
| '_'
......
......@@ -11,8 +11,6 @@
(** common functions to be used in lexers/parsers *)
val newline : Lexing.lexbuf -> unit
val comment : Lexing.lexbuf -> unit
val string : Lexing.lexbuf -> string
......
......@@ -23,11 +23,6 @@
| UnterminatedString -> fprintf fmt "unterminated string"
| _ -> raise e)
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let string_start_loc = ref Loc.dummy_position
let string_buf = Buffer.create 1024
......@@ -50,7 +45,7 @@ rule comment = parse
| "(*"
{ comment lexbuf; comment lexbuf }
| newline
{ newline lexbuf; comment lexbuf }
{ new_line lexbuf; comment lexbuf }
| eof
{ raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
| _
......@@ -62,11 +57,11 @@ and string = parse
Buffer.clear string_buf;
s }
| "\\" newline
{ newline lexbuf; string_skip_spaces lexbuf }
{ new_line lexbuf; string_skip_spaces lexbuf }
| "\\" (_ as c)
{ Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
| newline
{ newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
{ new_line lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
| eof
{ raise (Loc.Located (!string_start_loc, UnterminatedString)) }
| _ as c
......
......@@ -17,11 +17,6 @@
open Lexing
open Why3
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let backtrack lexbuf =
lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
lexbuf.lex_curr_p <- lexbuf.lex_start_p
......@@ -135,7 +130,7 @@ rule scan fmt empty delayed = parse
{ print_ident fmt lexbuf s;
scan fmt false delayed lexbuf }
| space* '\n'
{ newline lexbuf;
{ new_line lexbuf;
match empty, delayed with
| false, d ->
pp_print_char fmt '\n';
......@@ -165,7 +160,7 @@ and scan_isolated fmt empty in_pre delayed = parse
| eof { if in_pre then pp_print_string fmt "</pre>\n";
if delayed <> "" then pp_print_string fmt delayed }
| space* '\n'
{ newline lexbuf;
{ new_line lexbuf;
match empty, delayed with
| false, d | true, ("" as d) ->
scan_isolated fmt true in_pre d lexbuf
......@@ -188,7 +183,7 @@ and scan_embedded fmt depth = parse
| ident as s
{ print_ident fmt lexbuf s;
scan_embedded fmt depth lexbuf }
| "\n" { newline lexbuf;
| "\n" { new_line lexbuf;
pp_print_char fmt '\n';
scan_embedded fmt depth lexbuf }
| '"' { pp_print_string fmt "&quot;";
......@@ -204,7 +199,7 @@ and comment fmt do_output = parse
comment fmt do_output lexbuf }
| "*)" { if do_output then pp_print_string fmt "*)" }
| eof { () }
| "\n" { newline lexbuf;
| "\n" { new_line lexbuf;
if do_output then pp_print_char fmt '\n';
comment fmt do_output lexbuf }
| '"' { if do_output then pp_print_string fmt "&quot;";
......@@ -218,7 +213,7 @@ and comment fmt do_output = parse
comment fmt do_output lexbuf }
and string fmt do_output = parse
| "\n" { newline lexbuf;
| "\n" { new_line lexbuf;
if do_output then pp_print_char fmt '\n';
string fmt do_output lexbuf }
| '"' { if do_output then pp_print_string fmt "&quot;" }
......@@ -233,12 +228,12 @@ and doc fmt block headings = parse
| ' '* "*)"
{ if block then pp_print_string fmt "</p>\n" }
| eof { () }
| "\n" space* "\n" { newline lexbuf;
newline lexbuf;
| "\n" space* "\n" { new_line lexbuf;
new_line lexbuf;
if block then pp_print_string fmt "</p>";
pp_print_char fmt '\n';
doc fmt false headings lexbuf }
| "\n" { newline lexbuf;
| "\n" { new_line lexbuf;
pp_print_char fmt '\n';
doc fmt block headings lexbuf }
| '{' (['1'-'6'] as c) ' '*
......@@ -283,7 +278,7 @@ and doc fmt block headings = parse
and raw_html fmt depth = parse
| "*)" { backtrack lexbuf }
| eof { () }
| "\n" { newline lexbuf;
| "\n" { new_line lexbuf;
pp_print_char fmt '\n';
raw_html fmt depth lexbuf }
| '{' { pp_print_char fmt '{'; raw_html fmt (succ depth) lexbuf }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment