From: Stefano Zacchiroli Date: Fri, 4 Feb 2005 09:30:47 +0000 (+0000) Subject: parameterized lexer so that comment tokens could be returned or not, X-Git-Tag: V_0_1_0~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=394bf3a0ca050cf97b1f318363e2e353f67141ad;p=helm.git parameterized lexer so that comment tokens could be returned or not, per default they are not returned --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 9534704ed..6f179505d 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -106,8 +106,8 @@ let rec token' = lexer and token = lexer *) -let rec token = lexer - | blanks -> token lexbuf +let rec token comments = lexer + | blanks -> token comments lexbuf | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | ident -> let lexeme = Ulexing.utf8_lexeme lexbuf in @@ -132,26 +132,29 @@ let rec token = lexer with Utf8Macro.Macro_not_found _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) | comment -> - let comment = - Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 2) - in - return lexbuf ("COMMENT", comment) + if comments then + let comment = + Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 2) + in + return lexbuf ("COMMENT", comment) + else + token comments lexbuf | eof -> return lexbuf ("EOI", "") | _ -> error lexbuf "Invalid character" -let tok_func stream = +let tok_func comments stream = let lexbuf = Ulexing.from_utf8_stream stream in Token.make_stream_and_flocation (fun () -> try - token lexbuf + token comments lexbuf with | Ulexing.Error -> error_at_end lexbuf "Unexpected character" | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point") -let cic_lexer = - { - Token.tok_func = tok_func; +let cic_lexer ?(comments = false) () = + { + Token.tok_func = tok_func comments; Token.tok_using = (fun _ -> ()); Token.tok_removing = (fun _ -> ()); Token.tok_match = Token.default_match; diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli index 85ff08bce..7e3ac625b 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli @@ -25,5 +25,8 @@ exception Error of int * int * string -val cic_lexer : (string * string) Token.glexer + (** lexer + * @param comments if true the lexer will return COMMENT tokens, otherwise they + * will be ignored. Defaults to false *) +val cic_lexer: ?comments:bool -> unit -> (string * string) Token.glexer diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index e35101862..4bfc7c445 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -let debug = true +let debug = false let debug_print s = if debug then begin prerr_endline ""; @@ -35,12 +35,17 @@ let debug_print s = * thus be interpreted differently than others *) let use_fresh_num_instances = false + (** does the lexer return COMMENT tokens? *) +let return_comments = false + open Printf open DisambiguateTypes exception Parse_error of Token.flocation * string +let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () + let fresh_num_instance = let n = ref 0 in if use_fresh_num_instances then @@ -52,7 +57,7 @@ let choice_of_uri uri = let term = CicUtil.term_of_uri uri in (uri, (fun _ _ _ -> term)) -let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer +let grammar = Grammar.gcreate cic_lexer let term = Grammar.Entry.create grammar "term" let term0 = Grammar.Entry.create grammar "term0" @@ -525,7 +530,7 @@ EXTEND ]; script_entry: [ [ cmd = tactical0 -> Command cmd - | s = COMMENT -> Comment (loc, s) +(* | s = COMMENT -> Comment (loc, s) *) ] ]; script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; @@ -559,7 +564,7 @@ module EnvironmentP3 = let empty = "" - let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer + let aliases_grammar = Grammar.gcreate cic_lexer let aliases = Grammar.Entry.create aliases_grammar "aliases" let to_string env =