]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaScript.ml
ported to the new parser interface (Ulexing.lexbuf instead of char Stream.t)
[helm.git] / helm / matita / matitaScript.ml
index f12ac877dad2af34b1ca45fb31030d117861e322..a4f805bfb8e144aa74365e20a2e25fc03972b407 100644 (file)
@@ -369,7 +369,7 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
   if Pcre.pmatch ~rex:only_dust_RE unparsed_text then raise Margin;
   let st =
    try
-    GrafiteParser.parse_statement (Stream.of_string unparsed_text)
+    GrafiteParser.parse_statement (Ulexing.from_utf8_string unparsed_text)
    with
     CicNotationParser.Parse_error (floc,err) as exc ->
      let (x, y) = CicNotationPt.loc_of_floc floc in
@@ -730,7 +730,7 @@ object (self)
     let s = self#getFuture in
     let rec is_there_and_executable s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let st = GrafiteParser.parse_statement (Stream.of_string s) in
+      let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in
       match st with
       | GrafiteAst.Comment (loc,_)-> 
           let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in