From 358720b93255d1aa526dc03c63a5d6193658b93b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 13 Apr 2006 23:44:51 +0000 Subject: [PATCH] to tired to write a message. --- matita/.depend | 14 ++-- matita/Makefile | 4 +- matita/matitaEngine.ml | 2 +- matita/matitaExcPp.ml | 2 + matita/matitaGtkMisc.ml | 12 ++++ matita/matitaGtkMisc.mli | 8 +++ matita/matitaScript.ml | 137 ++++++++++++++++----------------------- 7 files changed, 90 insertions(+), 89 deletions(-) diff --git a/matita/.depend b/matita/.depend index 576d9dee8..2c41ea6ef 100644 --- a/matita/.depend +++ b/matita/.depend @@ -22,8 +22,10 @@ matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaExcPp.cmi matitaExcPp.cmx: matitaExcPp.cmi -matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo matitaGtkMisc.cmi -matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi +matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmi \ + matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ + matitaGtkMisc.cmi matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi @@ -49,11 +51,11 @@ matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmi applyTransformation.cmi \ - matitaScript.cmi + matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \ + applyTransformation.cmi matitaScript.cmi matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaScript.cmi + matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmo diff --git a/matita/Makefile b/matita/Makefile index b9755831a..af7445047 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -35,9 +35,9 @@ CMOS = \ matitaEngine.cmo \ matitacLib.cmo \ applyTransformation.cmo \ + matitaGtkMisc.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ - matitaGtkMisc.cmo \ matitaMathView.cmo \ matitaGui.cmo \ $(NULL) @@ -110,6 +110,8 @@ links: $(INSTALL_PROGRAMS_LINKS_MATITA); do\ ln -sf $$X.opt $$X;\ done + $(H)ln -sf matita.opt matita + $(H)ln -sf matitac.opt matitac matita: matita.ml $(LIB_DEPS) $(CMOS) $(H)echo " OCAMLC $<" diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml index f0d8ee46c..18022691c 100644 --- a/matita/matitaEngine.ml +++ b/matita/matitaEngine.ml @@ -93,7 +93,7 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status LexiconEngine.set_proof_aliases lexicon_status [k,value] in new_lexicon_status, - ((new_grafite_status,new_lexicon_status),Some (k,value))::acc + ((grafite_status,new_lexicon_status),Some (k,value))::acc ) (lexicon_status,[]) new_aliases in ((new_grafite_status,new_lexicon_status),None)::intermediate_states diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index ed0be4956..24608be42 100644 --- a/matita/matitaExcPp.ml +++ b/matita/matitaExcPp.ml @@ -62,6 +62,8 @@ let rec to_string = None, "Type checking assertion failed: " ^ Lazy.force msg | LibrarySync.AlreadyDefined s -> None, "Already defined: " ^ UriManager.string_of_uri s + | CoercDb.EqCarrNotImplemented msg -> + None, ("EqCarrNotImplemented: " ^ Lazy.force msg) | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> let rec aux n ?(dummy=false) (prev_msg,phases) = function diff --git a/matita/matitaGtkMisc.ml b/matita/matitaGtkMisc.ml index a41dbffe3..c397215a7 100644 --- a/matita/matitaGtkMisc.ml +++ b/matita/matitaGtkMisc.ml @@ -439,3 +439,15 @@ let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") GtkThread.main (); (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel) +let utf8_parsed_text s floc = + let start, stop = HExtlib.loc_of_floc floc in + let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in + let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in + let bytes = stop_bytes - start_bytes in + String.sub s start_bytes bytes, bytes + +let utf8_string_length s = + if BuildTimeConf.debug then + assert(Glib.Utf8.validate s); + Glib.Utf8.length s + diff --git a/matita/matitaGtkMisc.mli b/matita/matitaGtkMisc.mli index 1affd2a39..16b0591b2 100644 --- a/matita/matitaGtkMisc.mli +++ b/matita/matitaGtkMisc.mli @@ -155,3 +155,11 @@ val report_error: unit -> unit + (* given an utf8 string a floc returns the parsed substring and its length + * in bytes *) +val utf8_parsed_text: string -> Token.flocation -> string * int + + (* the length in characters, not bytes *) +val utf8_string_length: string -> int + + diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 4c40f9e14..62d760c3b 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -77,72 +77,33 @@ type guistuff = { } let eval_with_engine guistuff lexicon_status grafite_status user_goal - parsed_text st + skipped_txt nonskipped_txt st = let module TAPp = GrafiteAstPp in - let parsed_text_length = String.length parsed_text in - let initial_space,parsed_text = - try - let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in - let p1 = pieces.(1) in - let p1_len = String.length p1 in - let rest = String.sub parsed_text p1_len (parsed_text_length - p1_len) in - p1, rest - with - Not_found -> "", parsed_text in - let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' = - (* the code commented out adds the "select" command if needed *) - initial_space,grafite_status,lexicon_status,[] in -(* let loc, ex = - match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in - match grafite_status.proof_status with - | Incomplete_proof { stack = stack } - when not (List.mem user_goal (Continuationals.head_goals stack)) -> - let grafite_status = - MatitaEngine.eval_ast - ~do_heavy_checks:true grafite_status (goal_ast user_goal) - in - let initial_space = if initial_space = "" then "\n" else initial_space - in - "\n", grafite_status, - [ grafite_status, - initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] - | _ -> initial_space,grafite_status,[] in *) + let module DTE = DisambiguateTypes.Environment in + let module DP = DisambiguatePp in + let parsed_text_length = + String.length skipped_txt + String.length nonskipped_txt + in let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:true - new_lexicon_status new_grafite_status st + lexicon_status grafite_status st in - let _,new_text_list_rev = - let module DTE = DisambiguateTypes.Environment in - let module UM = UriManager in - List.fold_right ( - fun (_,alias) (initial_space,acc) -> + let enriched_history_fragment = List.rev enriched_history_fragment in + (* really fragile *) + let res,_ = + List.fold_left + (fun (acc, to_prepend) (status,alias) -> match alias with - None -> initial_space,initial_space::acc - | Some (k,((v,_) as value)) -> - let new_text = - let initial_space = - if initial_space = "" then "\n" else initial_space - in - initial_space ^ - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - DisambiguateTypes.Environment.empty) - in - "\n",new_text::acc - ) enriched_history_fragment (initial_space,[]) in - let new_text_list_rev = - match enriched_history_fragment,new_text_list_rev with - (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl - | _,_ -> assert false + | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" + | Some (k,((v,_) as value)) -> + let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in + (status,to_prepend ^ newtxt ^ "\n")::acc, "") + ([],skipped_txt) enriched_history_fragment in - let res = - try - List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev - with - Invalid_argument _ -> assert false - in - res,parsed_text_length + let res = (*List.combine (List.map fst (List.rev enriched_history_fragment)) + strings*) res in + res,parsed_text_length let wrap_with_developments guistuff f arg = try @@ -201,11 +162,13 @@ let wrap_with_developments guistuff f arg = ;; let eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text st + guistuff lexicon_status grafite_status user_goal + skipped_txt nonskipped_txt st = wrap_with_developments guistuff (eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text) st + guistuff lexicon_status grafite_status user_goal + skipped_txt nonskipped_txt) st ;; let pp_eager_statement_ast = @@ -287,7 +250,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let text = comment parsed_text ^ "\n" ^ pp_eager_statement_ast (ast HExtlib.dummy_floc) in - let text_len = String.length text in + let text_len = MatitaGtkMisc.utf8_string_length text in let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in let res,_parsed_text_len = @@ -319,7 +282,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status | TA.Search_pat (_, search_kind, str) -> failwith "not implemented" | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex +and eval_executable include_paths (buffer : GText.buffer) guistuff +lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt +script ex loc = let module TAPp = GrafiteAstPp in let module MD = GrafiteDisambiguator in @@ -345,7 +310,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu | _ -> () end; eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text + guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], 0 @@ -356,7 +321,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu | Some n -> GrafiteTypes.get_proof_context grafite_status n in let grafite_status,macro = lazy_macro context in eval_macro include_paths buffer guistuff lexicon_status grafite_status - user_goal unparsed_text parsed_text script macro + user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal script statement @@ -373,18 +338,22 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status ast, text | `Ast (st, text) -> (lexicon_status, st), text in - let text_of_loc loc = - let parsed_text_length = snd (HExtlib.loc_of_floc loc) in - let parsed_text = safe_substring unparsed_text 0 parsed_text_length in - parsed_text, parsed_text_length - in + let text_of_loc floc = + let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let start, stop = HExtlib.loc_of_floc floc in + let floc = HExtlib.floc_of_loc (0, start) in + let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let floc = HExtlib.floc_of_loc (0, stop) in + let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + txt,nonskipped_txt,skipped_txt,len + in match st with | GrafiteParser.LNone loc -> - let parsed_text, parsed_text_length = text_of_loc loc in + let parsed_text, _, _, parsed_text_length = text_of_loc loc in [(grafite_status,lexicon_status),parsed_text], parsed_text_length | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> - let parsed_text, parsed_text_length = text_of_loc loc in + let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in let s,len = @@ -404,9 +373,11 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status (statuses,parsed_text ^ text)::tl,parsed_text_length + len | [] -> [], 0) | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let parsed_text, parsed_text_length = text_of_loc loc in + let _, nonskipped, skipped, parsed_text_length = + text_of_loc loc + in eval_executable include_paths buffer guistuff lexicon_status - grafite_status user_goal unparsed_text parsed_text script loc ex + grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = let i = ref 0 in @@ -506,12 +477,14 @@ object (self) if statement <> None then buffer#insert ~iter:start new_text else begin - if new_text <> String.sub s 0 parsed_len then begin - buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len); + let parsed_text = String.sub s 0 parsed_len in + if new_text <> parsed_text then begin + let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in + buffer#delete ~start ~stop; buffer#insert ~iter:start new_text; end; end; - self#moveMark (String.length new_text); + self#moveMark (Glib.Utf8.length new_text); (* here we need to set the Goal in case we are going to cursor (or to bottom) and we will face a macro *) match self#grafite_status.proof_status with @@ -547,7 +520,8 @@ object (self) let cmp,new_statements,new_history,(grafite_status,lexicon_status) = match statements,history with stat::statements, _::(status::_ as history) -> - String.length stat, statements, history, status + assert (Glib.Utf8.validate stat); + Glib.Utf8.length stat, statements, history, status | [],[_] -> raise Margin | _,_ -> assert false in @@ -789,7 +763,6 @@ object (self) method goal = userGoal method eos = - let s = self#getFuture in let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let lexicon_status,st = @@ -798,7 +771,9 @@ object (self) in match st with | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> - let parsed_text_length = snd (HExtlib.loc_of_floc loc) in + let _,parsed_text_length = + MatitaGtkMisc.utf8_parsed_text s loc + in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_only_comments lexicon_status next @@ -806,7 +781,7 @@ object (self) | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in try - is_there_only_comments self#lexicon_status s + is_there_only_comments self#lexicon_status self#getFuture with | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false -- 2.39.2