Commit 8ed7c5ec authored by Sylvain Dailler's avatar Sylvain Dailler

ide: Use a different color on parsing error

By default, the color used for font errors in the messages view is used
as background for precise locations of errors in source.
Perhaps, its a good idea to change the color in the future.
parent de3e12ff
......@@ -249,11 +249,14 @@ let create_colors v =
~name:"error_line_tag" [`BACKGROUND gconfig.error_line_color] in
let error_tag (v: GSourceView.source_view) = v#buffer#create_tag
~name:"error_tag" [`BACKGROUND gconfig.error_color_bg] in
let error_font_tag (v: GSourceView.source_view) = v#buffer#create_tag
~name:"error_font_tag" [`BACKGROUND gconfig.error_color] in
let _ : GText.tag = premise_tag v in
let _ : GText.tag = neg_premise_tag v in
let _ : GText.tag = goal_tag v in
let _ : GText.tag = error_line_tag v in
let _ : GText.tag = error_tag v in
let _ : GText.tag = error_font_tag v in
()
(* Erase all the source location tags in a source file *)
......@@ -263,7 +266,8 @@ let erase_color_loc (v:GSourceView.source_view) =
buf#remove_tag_by_name "neg_premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "goal_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "error_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "error_line_tag" ~start:buf#start_iter ~stop:buf#end_iter
buf#remove_tag_by_name "error_line_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "error_font_tag" ~start:buf#start_iter ~stop:buf#end_iter
......@@ -1060,6 +1064,7 @@ let convert_color (color: color): string =
| Goal_color -> "goal_tag"
| Error_color -> "error_tag"
| Error_line_color -> "error_line_tag"
| Error_font_color -> "error_font_tag"
let color_line ~color loc =
let color_line (v:GSourceView.source_view) ~color l =
......@@ -1534,7 +1539,7 @@ let treat_message_notification msg = match msg with
begin
scroll_to_loc ~force_tab_switch:true (Some loc);
color_line ~color:Error_line_color loc;
color_loc ~color:Error_color loc;
color_loc ~color:Error_font_color loc;
print_message ~kind:1 ~notif_kind:"Parse_Or_Type_Error" "%s" s
end
else
......
......@@ -66,6 +66,7 @@ type color =
| Goal_color
| Error_color
| Error_line_color
| Error_font_color
type update_info =
| Proved of bool
......
......@@ -76,6 +76,7 @@ type color =
| Goal_color
| Error_color
| Error_line_color
| Error_font_color
type update_info =
| Proved of bool
......
......@@ -313,7 +313,9 @@ let convert_color (color: color) : Json_base.json =
| Premise_color -> "Premise_color"
| Goal_color -> "Goal_color"
| Error_color -> "Error_color"
| Error_line_color -> "Error_line_color")
| Error_line_color -> "Error_line_color"
| Error_font_color -> "Error_font_color"
)
let convert_loc_color (loc,color: Loc.position * color) : Json_base.json =
let loc = convert_loc loc in
......@@ -333,6 +335,7 @@ let parse_color (j: json) : color =
| String "Goal_color" -> Goal_color
| String "Error_color" -> Error_color
| String "Error_line_color" -> Error_line_color
| String "Error_font_color" -> Error_font_color
| _ -> raise Notcolor
exception Notposition
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment