From 33b362600b2756274258f06f26a08c918ec28062 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 21 Sep 2005 14:40:59 +0000 Subject: [PATCH] ported to the new parser interface (Ulexing.lexbuf instead of char Stream.t) --- helm/matita/matitaEngine.ml | 5 +++-- helm/matita/matitaEngine.mli | 4 ++-- helm/matita/matitaMisc.ml | 2 +- helm/matita/matitaScript.ml | 4 ++-- helm/matita/matitacLib.ml | 4 ++-- helm/matita/matitadep.ml | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 +++- helm/ocaml/cic_disambiguation/disambiguatePp.ml | 2 +- 8 files changed, 15 insertions(+), 12 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 3658b0c20..0cab549b1 100644 --- 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 280b6c8f4..2253748d9 100644 --- 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 97d6cac47..c67602dba 100644 --- 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 f12ac877d..a4f805bfb 100644 --- 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 209919980..b30a55234 100644 --- 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 9fafa4907..5a73c099b 100644 --- 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 6dbd31248..054826cca 100644 --- 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 b7c1012a8..4bf917bb8 100644 --- 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 -- 2.39.2