diff options
| author | Pierre-Marie Pédrot | 2016-05-31 13:33:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-31 13:33:01 +0200 |
| commit | 27dffdea5b46f6282c1584db0555213e744352fa (patch) | |
| tree | 3f89cd9e8828f1ca1c8a1c10d74f020dcb7543f1 /toplevel | |
| parent | cb31cd671a0ef4da0cf834dad5b67776098bb0d1 (diff) | |
Revert "Rename Lexer -> CLexer."
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 14 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 8 |
5 files changed, 15 insertions, 15 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index d8ee5d90da..600683d359 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -35,7 +35,7 @@ let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) + | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 040c339249..063ed89643 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -288,7 +288,7 @@ let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () + | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot () | End_of_input -> raise End_of_input | e when Errors.noncritical e -> () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 08b38a7037..9e1a76bbd6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -230,11 +230,11 @@ let compile_files () = | [vf] -> compile_file vf (* One compilation : no need to save init state *) | l -> let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = CLexer.location_table () in + let coqdoc_init_state = Lexer.location_table () in List.iter (fun vf -> States.unfreeze init_state; - CLexer.restore_location_table coqdoc_init_state; + Lexer.restore_location_table coqdoc_init_state; compile_file vf) (List.rev l) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c33726550d..2ccd27acb9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -31,7 +31,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = CLexer.add_keyword s +let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with @@ -428,7 +428,7 @@ let rec interp_list_parser hd = function (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = CLexer.is_ident x in + let norm = Lexer.is_ident x in if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'" else x @@ -436,7 +436,7 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when CLexer.is_ident x -> + | String x :: sl when Lexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl @@ -725,7 +725,7 @@ let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; + Lexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] @@ -734,7 +734,7 @@ let rec define_keywords_aux = function let define_keywords = function | GramConstrTerminal(IDENT k)::l -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; + Lexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -763,12 +763,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in distribute [GramConstrNonTerminal (typ, Some m)] ll | Terminal s -> - distribute [GramConstrTerminal (CLexer.terminal s)] ll + distribute [GramConstrTerminal (Lexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] + (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in match List.assoc x etyps with diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a5f502503b..7c4920dfb8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -164,17 +164,17 @@ let save_translator_coqdoc () = (* translator state *) let ch = !chan_beautify in let cl = !Pp.comments in - let cs = CLexer.com_state() in + let cs = Lexer.com_state() in (* end translator state *) - let coqdocstate = CLexer.location_table () in + let coqdocstate = Lexer.location_table () in ch,cl,cs,coqdocstate let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Pp.comments := cl; - CLexer.restore_com_state cs; - CLexer.restore_location_table coqdocstate + Lexer.restore_com_state cs; + Lexer.restore_location_table coqdocstate (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) |
