ported to the new parser interface (Ulexing.lexbuf instead of char Stream.t)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3658b0c20ab93d2990a9a73717faaf35c87bf463..0cab549b1345e31f86d47a7aba708807576064d4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -709,7 +709,7 @@ let eval_command opts status cmd =
      let ic =
       try open_in moopath with Sys_error _ -> 
         raise (IncludedFileNotCompiled moopath) in
-     let stream = Stream.of_channel ic in
+     let stream = Ulexing.from_utf8_channel ic in
      let status = ref status in
       profiler_include.CicUtil.profile
        (!eval_from_stream_ref status stream) (fun _ _ -> ());
@@ -914,7 +914,8 @@ let eval_from_stream_greedy
 
 let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
   eval_from_stream 
-    ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
+    ?do_heavy_checks ?include_paths ?clean_baseuri status
+      (Ulexing.from_utf8_string str) (fun _ _ ->())
 
 let default_options () =
 (*

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index 280b6c8f47d273a6cac415b3feb8eb52e487e6c4..2253748d95b61efd1f5a060743aed50c18e23e03 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -44,7 +44,7 @@ val eval_from_stream:
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
   ?clean_baseuri:bool ->
-  MatitaTypes.status ref -> char Stream.t -> 
+  MatitaTypes.status ref -> Ulexing.lexbuf -> 
   (MatitaTypes.status -> statement -> unit) ->
     unit
 
@@ -52,7 +52,7 @@ val eval_from_stream_greedy:
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
   ?clean_baseuri:bool ->
-  MatitaTypes.status ref-> char Stream.t -> 
+  MatitaTypes.status ref-> Ulexing.lexbuf -> 
   (MatitaTypes.status -> statement -> unit) ->
     unit
 

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 97d6cac4738b2b0a12c53ceaaad7cfc99d19dda5..c67602dbac3065f00745a9c4aea2fe1fae0c5a55 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -41,7 +41,7 @@ let baseuri_of_baseuri_decl st =
 let baseuri_of_file file = 
   let uri = ref None in
   let ic = open_in file in
-  let istream = Stream.of_channel ic in
+  let istream = Ulexing.from_utf8_channel ic in
   (try
     while true do
       try 

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f12ac877dad2af34b1ca45fb31030d117861e322..a4f805bfb8e144aa74365e20a2e25fc03972b407 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 209919980790fdaceabe4352511d9be41b8b6647..b30a55234b94f12d80c6330eefac65bba5de2636 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -127,7 +127,7 @@ let clean_exit n =
        opt_exit n
   
 let rec interactive_loop () = 
- let str = Stream.of_channel stdin in
+  let str = Ulexing.from_utf8_channel stdin in
   try
     run_script str 
       (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in)
@@ -186,7 +186,7 @@ let main ~mode =
     else
       MatitaLog.message (sprintf "execution of %s started:" fname);
     let is =
-      Stream.of_channel
+      Ulexing.from_utf8_channel
         (match fname with
         | "stdin" -> stdin
         | fname -> open_in fname)

diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index 9fafa4907f3dd54f83c20777e69baf44363cc038..5a73c099bee3866cd1d8294c3a6e8e0e13c5c573 100644 (file)
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -74,7 +74,7 @@ let main () =
   List.iter
    (fun file -> 
     let ic = open_in file in
-    let istream = Stream.of_channel ic in
+    let istream = Ulexing.from_utf8_channel ic in
     let dependencies = GrafiteParser.parse_dependencies istream in
     close_in ic;
     List.iter 

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6dbd312481a0c50e52ef7173787895a0a60bfb14..054826ccae24aed0e7d5d27e0f1bc153fe675875 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -909,7 +909,9 @@ struct
   let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
     ?(aliases = DisambiguateTypes.Environment.empty) term
   =
-    let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
+    let ast =
+      CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
+    in
     try
       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
         ?initial_ugraph ~aliases ~universe:None)

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index b7c1012a8dc68474e2515f567320f82a4c7bbe8d..4bf917bb8a9a4e5a2f757884d7484dd2690936c3 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -26,7 +26,7 @@
 open DisambiguateTypes
 
 let parse_environment str =
- let stream = Stream.of_string str in
+ let stream = Ulexing.from_utf8_string str in
  let environment = ref Environment.empty in
  let multiple_environment = ref Environment.empty in
   try