From: Stefano Zacchiroli <zack@upsilon.cc>
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 "<NEW_TEXTUAL_PARSER>";
@@ -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 =