X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=4bfc7c4457ba7ea6f9be44469e1811bf071052d9;hb=9983d0f08f594ddc01700c972d2a2c0f47d32d59;hp=e35101862cb0c6137fa0b6f69b3b12a1be8019ff;hpb=caede9392c6fb7988731e0bbd1d1c42817f443de;p=helm.git

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 =