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\" \"<uri>\".' 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
(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
* http://helm.cs.unibo.it/
*)
-val to_string: exn -> string
+val to_string: exn -> Token.flocation option * string
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 <- []));
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
| 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
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 ->
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 *)
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
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
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
method locked_mark : Gtk.text_mark
method locked_tag : GText.tag
+ method error_tag : GText.tag
(** @return current status *)
method status: MatitaTypes.status
| 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 () =
| 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 ()
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)
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);
projects / helm.git / commitdiff