X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Lexer.mll;h=0ef38a919b55604548d120eaf607004d2d961e52;hb=f620bf94af6c347926ed1c2328462efab7018b21;hp=57f7d16ae1bff92121e55c2b05bbefc357a99600;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git

diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll
index 57f7d16ae..0ef38a919 100644
--- a/helm/software/components/binaries/transcript/v8Lexer.mll
+++ b/helm/software/components/binaries/transcript/v8Lexer.mll
@@ -1,7 +1,17 @@
 {
+   module O = Options
    module P = V8Parser
    
-   let out t s = prerr_endline (t ^ " " ^ s)
+   let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s)
+
+   let check s =
+      let c = Char.code s.[0] in
+      if c <= 127 then s else 
+      let escaped = Printf.sprintf "\\%3u\\" c in
+      begin 
+         if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped;
+	 escaped 
+      end
 }
 
 let QT    = '"'
@@ -89,6 +99,6 @@ rule token = parse
    | ";"           { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s      }
    | ":"           { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s      }
    | ","           { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s      }
-   | ".."          { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s }
-   | _             { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s }
+   | _             
+      { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s }
    | eof           { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF      }