X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftext%2FtxtLexer.mll;h=eea312714cda955fb53d9ed1a62892980f09b8de;hb=1eb848417fefd0ef7436d4a89e59535baf9632c7;hp=ec97a8b83489c98fd833a43e69f65ae2faa67014;hpb=f72311aa07e71090a24eef9e4fb97cc2e95e6b16;p=helm.git

diff --git a/helm/software/helena/src/text/txtLexer.mll b/helm/software/helena/src/text/txtLexer.mll
index ec97a8b83..eea312714 100644
--- a/helm/software/helena/src/text/txtLexer.mll
+++ b/helm/software/helena/src/text/txtLexer.mll
@@ -15,8 +15,10 @@
    module TP = TxtParser
 
    let level = 0
-   
+
+IFDEF LEXER THEN   
    let out s = if !G.debug_lexer then L.warn level s else ()
+END
 }
 
 let BS    = "\\"
@@ -42,36 +44,37 @@ and qstring = parse
 and token = parse
    | SPC          { token lexbuf                                         } 
    | OC           { block_comment lexbuf; token lexbuf                   }
-   | ID as id     { out ("ID " ^ id); TP.ID id                           }
-   | IX as ix     { out ("IX " ^ ix); TP.IX (int_of_string ix)           }
-   | QT           { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s }
-   | "\\graph"    { out "GRAPH"; TP.GRAPH }
-   | "\\main"     { out "MAIN"; TP.MAIN   }
-   | "\\decl"     { out "DECL"; TP.DECL   }
-   | "\\ax"       { out "AX"; TP.AX       }
-   | "\\cong"     { out "CONG"; TP.CONG   }
-   | "\\def"      { out "DEF"; TP.DEF     }
-   | "\\th"       { out "TH"; TP.TH       }
-   | "\\generate" { out "GEN"; TP.GEN     }
-   | "\\require"  { out "REQ"; TP.REQ     }
-   | "\\open"     { out "OPEN"; TP.OPEN   } 
-   | "\\close"    { out "CLOSE"; TP.CLOSE }
-   | "\\sorts"    { out "SORTS"; TP.SORTS }
-   | "("          { out "OP"; TP.OP       }
-   | ")"          { out "CP"; TP.CP       }
-   | "["          { out "OB"; TP.OB       }
-   | "]"          { out "CB"; TP.CB       }
-   | "<"          { out "OA"; TP.OA       }
-   | ">"          { out "CA"; TP.CA       }
-   | "."          { out "FS"; TP.FS       }   
-   | ":"          { out "CN"; TP.CN       }   
-   | ","          { out "CM"; TP.CM       }
-   | "="          { out "EQ"; TP.EQ       }
-   | "*"          { out "STAR"; TP.STAR   }
-   | "#"          { out "HASH"; TP.HASH   }
-   | "+"          { out "PLUS"; TP.PLUS   }
-   | "~"          { out "TE"; TP.TE       }
-   | "->"         { out "WTO"; TP.WTO     }
-   | "=>"         { out "STO"; TP.STO     }
-   | "^"          { out "CT"; TP.CT       }
-   | eof          { out "EOF"; TP.EOF     }
+   | ID as id     { IFDEF LEXER THEN out ("ID " ^ id) ELSE () END; TP.ID id                 }
+   | IX as ix     { IFDEF LEXER THEN out ("IX " ^ ix) ELSE () END; TP.IX (int_of_string ix) }
+   | QT           { let s = qstring lexbuf in
+                    IFDEF LEXER THEN out ("STR " ^ s) ELSE () END; TP.STR s
+                  }
+   | "\\graph"    { IFDEF LEXER THEN out "GRAPH" ELSE () END; TP.GRAPH }
+   | "\\main"     { IFDEF LEXER THEN out "MAIN" ELSE () END; TP.MAIN   }
+   | "\\decl"     { IFDEF LEXER THEN out "DECL" ELSE () END; TP.DECL   }
+   | "\\ax"       { IFDEF LEXER THEN out "AX" ELSE () END; TP.AX       }
+   | "\\cong"     { IFDEF LEXER THEN out "CONG" ELSE () END; TP.CONG   }
+   | "\\def"      { IFDEF LEXER THEN out "DEF" ELSE () END; TP.DEF     }
+   | "\\th"       { IFDEF LEXER THEN out "TH" ELSE () END; TP.TH       }
+   | "\\generate" { IFDEF LEXER THEN out "GEN" ELSE () END; TP.GEN     }
+   | "\\require"  { IFDEF LEXER THEN out "REQ" ELSE () END; TP.REQ     }
+   | "\\open"     { IFDEF LEXER THEN out "OPEN" ELSE () END; TP.OPEN   } 
+   | "\\close"    { IFDEF LEXER THEN out "CLOSE" ELSE () END; TP.CLOSE }
+   | "\\sorts"    { IFDEF LEXER THEN out "SORTS" ELSE () END; TP.SORTS }
+   | "("          { IFDEF LEXER THEN out "OP" ELSE () END; TP.OP       }
+   | ")"          { IFDEF LEXER THEN out "CP" ELSE () END; TP.CP       }
+   | "["          { IFDEF LEXER THEN out "OB" ELSE () END; TP.OB       }
+   | "]"          { IFDEF LEXER THEN out "CB" ELSE () END; TP.CB       }
+   | "{"          { IFDEF LEXER THEN out "OC" ELSE () END; TP.OC       }
+   | "}"          { IFDEF LEXER THEN out "CC" ELSE () END; TP.CC       }
+   | "<"          { IFDEF LEXER THEN out "OA" ELSE () END; TP.OA       }
+   | ">"          { IFDEF LEXER THEN out "CA" ELSE () END; TP.CA       }
+   | "."          { IFDEF LEXER THEN out "FS" ELSE () END; TP.FS       }   
+   | ":"          { IFDEF LEXER THEN out "CN" ELSE () END; TP.CN       }   
+   | ","          { IFDEF LEXER THEN out "CM" ELSE () END; TP.CM       }
+   | "="          { IFDEF LEXER THEN out "EQ" ELSE () END; TP.EQ       }
+   | "*"          { IFDEF LEXER THEN out "STAR" ELSE () END; TP.STAR   }
+   | "#"          { IFDEF LEXER THEN out "HASH" ELSE () END; TP.HASH   }
+   | "~"          { IFDEF LEXER THEN out "TE" ELSE () END; TP.TE       }
+   | "^"          { IFDEF LEXER THEN out "CT" ELSE () END; TP.CT       }
+   | eof          { IFDEF LEXER THEN out "EOF" ELSE () END; TP.EOF     }