From 78cd354ba5225f6431ab0bab6dcaa548bb5a24c3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 Nov 2005 22:31:36 +0000 Subject: [PATCH] New implementation for localized exceptions. --- helm/matita/matitaExcPp.ml | 41 ++++++++++++++----------- helm/matita/matitaExcPp.mli | 2 +- helm/matita/matitaGui.ml | 30 ++++++++++++++++++- helm/matita/matitaMathView.ml | 2 +- helm/matita/matitaScript.ml | 56 +++++++++-------------------------- helm/matita/matitaScript.mli | 1 + helm/matita/matitacLib.ml | 10 +++---- helm/matita/matitacleanLib.ml | 2 +- 8 files changed, 76 insertions(+), 68 deletions(-) diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index 3ad6da153..2d0f60c9e 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -25,36 +25,42 @@ open Printf -let to_string = +let rec to_string = function + | HExtlib.Localized (floc,exn) -> + let _,msg = to_string exn in + let (x, y) = HExtlib.loc_of_floc floc in + Some floc, sprintf "Error at %d-%d: %s" x y msg | MatitaTypes.Option_error ("baseuri", "not found" ) -> + None, "Baseuri not set for this script. " ^ "Use 'set \"baseuri\" \"\".' to set it." - | MatitaTypes.Command_error msg -> "Error: " ^ msg - | CicNotationParser.Parse_error (floc,err) -> - let (x, y) = CicNotationPt.loc_of_floc floc in - sprintf "Parse error at %d-%d: %s" x y err - | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri + | MatitaTypes.Command_error msg -> None, "Error: " ^ msg + | CicNotationParser.Parse_error err -> + None, sprintf "Parse error: %s" err + | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri | CicEnvironment.Object_not_found uri -> - sprintf "object not found: %s" (UriManager.string_of_uri uri) + None, sprintf "object not found: %s" (UriManager.string_of_uri uri) | Unix.Unix_error (code, api, param) -> let err = Unix.error_message code in - "Unix Error (" ^ api ^ "): " ^ err + None, "Unix Error (" ^ api ^ "): " ^ err | MatitaMoo.Corrupt_moo fname -> - sprintf ".moo file '%s' is corrupt (shorter than expected)" fname + None, sprintf ".moo file '%s' is corrupt (shorter than expected)" fname | MatitaMoo.Checksum_failure fname -> - sprintf "checksum failed for .moo file '%s', please recompile it'" fname + None, + sprintf "checksum failed for .moo file '%s', please recompile it'" fname | MatitaMoo.Version_mismatch fname -> + None, sprintf (".moo file '%s' has been compiled by a different version of matita, " ^^ "please recompile it") fname - | ProofEngineTypes.Fail msg -> "Tactic error: " ^ Lazy.force msg - | Continuationals.Error s -> "Tactical error: " ^ Lazy.force s + | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg + | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s | CicTypeChecker.TypeCheckerFailure msg -> - "Type checking error: " ^ Lazy.force msg + None, "Type checking error: " ^ Lazy.force msg | CicTypeChecker.AssertFailure msg -> - "Type checking assertion failed: " ^ Lazy.force msg + None, "Type checking assertion failed: " ^ Lazy.force msg | MatitaDisambiguator.DisambiguationError errorll -> let rec aux n = function @@ -66,7 +72,8 @@ let to_string = (List.map (fun msg -> "*Error: " ^ Lazy.force msg) phase) ^ "\n\n\n" in - "********** DISAMBIGUATION ERRORS: **********\n" ^ - aux 1 errorll - | exn -> "Uncaught exception: " ^ Printexc.to_string exn + None, + "********** DISAMBIGUATION ERRORS: **********\n" ^ + aux 1 errorll + | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/matita/matitaExcPp.mli b/helm/matita/matitaExcPp.mli index 4c4eddc8d..9d8c7739f 100644 --- a/helm/matita/matitaExcPp.mli +++ b/helm/matita/matitaExcPp.mli @@ -23,5 +23,5 @@ * http://helm.cs.unibo.it/ *) -val to_string: exn -> string +val to_string: exn -> Token.flocation option * string diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index fe113743b..853168b29 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -574,7 +574,35 @@ class gui () = GtkSignal.user_handler := (fun exn -> if not (Helm_registry.get_bool "matita.debug") then - MatitaLog.error (MatitaExcPp.to_string exn) + let floc, msg = MatitaExcPp.to_string exn in + begin + match floc with + None -> () + | Some floc -> + let (x, y) = HExtlib.loc_of_floc floc in + let script = MatitaScript.current () in + let locked_mark = script#locked_mark in + let error_tag = script#error_tag in + let baseoffset = + (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in + let x' = baseoffset + x in + let y' = baseoffset + y in + let x_iter = source_buffer#get_iter (`OFFSET x') in + let y_iter = source_buffer#get_iter (`OFFSET y') in + source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; + let id = ref None in + id := Some (source_buffer#connect#changed ~callback:(fun () -> + source_buffer#remove_tag error_tag + ~start:source_buffer#start_iter + ~stop:source_buffer#end_iter; + match !id with + | None -> assert false (* a race condition occurred *) + | Some id -> + (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id)); + source_buffer#place_cursor + (source_buffer#get_iter (`OFFSET x')); + end; + MatitaLog.error msg else raise exn); (* script *) ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- [])); diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 710efdf02..507837c15 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -672,7 +672,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) f () with exn -> if not (Helm_registry.get_bool "matita.debug") then - fail (MatitaExcPp.to_string exn) + fail (snd (MatitaExcPp.to_string exn)) else raise exn in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 34e0408c5..4413f9b8a 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -372,49 +372,18 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script | TA.Macro (_,mac) -> eval_macro guistuff status user_goal unparsed_text parsed_text script mac -let parse_statement baseoffset parsedlen ?error_tag (buffer: GText.buffer) text -= - try - GrafiteParser.parse_statement (Ulexing.from_utf8_string text) - with CicNotationParser.Parse_error (floc, err) as exn -> - match error_tag with - | None -> raise exn - | Some error_tag -> - let (x, y) = CicNotationPt.loc_of_floc floc in - let x = parsedlen + x in - let y = parsedlen + y in - let x' = baseoffset + x in - let y' = baseoffset + y in - let x_iter = buffer#get_iter (`OFFSET x') in - let y_iter = buffer#get_iter (`OFFSET y') in - buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; - let id = ref None in - id := Some (buffer#connect#changed ~callback:(fun () -> - buffer#remove_tag error_tag ~start:buffer#start_iter - ~stop:buffer#end_iter; - match !id with - | None -> assert false (* a race condition occurred *) - | Some id -> - (new GObj.gobject_ops buffer#as_buffer)#disconnect id)); - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in - buffer#place_cursor (buffer#get_iter (`OFFSET x')); - raise (CicNotationParser.Parse_error (floc, err)) - -let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) - guistuff status user_goal script statement +let rec eval_statement (buffer : GText.buffer) guistuff status user_goal + script statement = let st, unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - parse_statement baseoffset parsedlen ~error_tag buffer text, text + GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text | `Ast (st, text) -> st, text in let text_of_loc loc = - let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in + 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 @@ -424,8 +393,12 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) 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 = - eval_statement baseoffset (parsedlen + parsed_text_length) error_tag - buffer guistuff status user_goal script (`Raw s) + try + eval_statement buffer guistuff status user_goal script + (`Raw s) + with HExtlib.Localized (floc, exn) -> + HExtlib.raise_localized_exception + ~offset:parsed_text_length floc exn in (match s with | (status, (text, ast)) :: tl -> @@ -494,6 +467,7 @@ object (self) method locked_mark = locked_mark method locked_tag = locked_tag + method error_tag = error_tag (* history can't be empty, the invariant above grant that it contains at * least the init status *) @@ -501,10 +475,8 @@ object (self) method private _advance ?statement () = let rec aux st = - let baseoffset = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in let (entries, parsed_len) = - eval_statement baseoffset 0 error_tag buffer guistuff self#status - userGoal self st + eval_statement buffer guistuff self#status userGoal self st in let (new_statuses, new_statements, new_asts) = let statuses, statements = List.split entries in @@ -534,7 +506,7 @@ object (self) in let text = self#getFuture in (try - (match parse_statement baseoffset 0 ?error_tag:None buffer text with + (match parse_statement baseoffset 0 buffer text with | TA.Executable (loc, TA.Tactical (_, tac, None)) as st when GrafiteAst.is_punctuation tac -> let len = snd (CicNotationPt.loc_of_floc loc) in @@ -774,7 +746,7 @@ object (self) 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 + let parsed_text_length = snd (HExtlib.loc_of_floc 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_and_executable next diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 35ae43ebb..f3523c15b 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -28,6 +28,7 @@ object method locked_mark : Gtk.text_mark method locked_tag : GText.tag + method error_tag : GText.tag (** @return current status *) method status: MatitaTypes.status diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 8552cbf86..872dccace 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -61,7 +61,7 @@ let run_script is eval_function = | End_of_file | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> - MatitaLog.error (MatitaExcPp.to_string exn); + MatitaLog.error (snd (MatitaExcPp.to_string exn)); raise exn let fname () = @@ -107,8 +107,8 @@ let rec interactive_loop () = | End_of_file -> print_newline (); clean_exit (Some 0) - | CicNotationParser.Parse_error (floc,err) -> - let (x, y) = CicNotationPt.loc_of_floc floc in + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let (x, y) = HExtlib.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); interactive_loop () | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop () @@ -200,8 +200,8 @@ let main ~mode = clean_exit (Some 1) else pp_ocaml_mode () - | CicNotationParser.Parse_error (floc,err) -> - let (x, y) = CicNotationPt.loc_of_floc floc in + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let (x, y) = HExtlib.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); if mode = `COMPILER then clean_exit (Some 1) diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 82fac08af..a4156921d 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -252,7 +252,7 @@ let baseuri_of_file file = with CicNotationParser.Parse_error _ as exn -> prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exn); + prerr_endline (snd (MatitaExcPp.to_string exn)); () done with End_of_file -> close_in ic); -- 2.39.2