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 9534704edd466caeabd591cc9ed6ebf84ef8b7d2..6f179505d749c8782e7a83b2ff58edc1bde3b964 100644 (file)
--- 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 85ff08bcee4fc9cb6e5510782c38a64d97cf878d..7e3ac625bc3625fbf47e48392ec43fd7953a4546 100644 (file)
--- 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 e35101862cb0c6137fa0b6f69b3b12a1be8019ff..4bfc7c4457ba7ea6f9be44469e1811bf071052d9 100644 (file)
--- 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 =