Commit fb5858f6 authored by Andrei Paskevich's avatar Andrei Paskevich

minor

rename location_color to goal_color and lighter_location_color
to premise_color
parent d6769827
......@@ -41,8 +41,8 @@ type t =
mutable show_locs : bool;
mutable saving_policy : int;
(** 0 = always, 1 = never, 2 = ask *)
mutable lighter_location_color : string;
mutable location_color : string;
mutable premise_color : string;
mutable goal_color : string;
mutable error_color : string;
(** colors *)
mutable env : Env.env;
......@@ -60,8 +60,8 @@ type ide = {
ide_show_labels : bool;
ide_show_locs : bool;
ide_saving_policy : int;
ide_lighter_location_color : string;
ide_location_color : string;
ide_premise_color : string;
ide_goal_color : string;
ide_error_color : string;
ide_default_editor : string;
}
......@@ -76,8 +76,8 @@ let default_ide =
ide_show_labels = false;
ide_show_locs = false;
ide_saving_policy = 0;
ide_lighter_location_color = "chartreuse";
ide_location_color = "gold";
ide_premise_color = "chartreuse";
ide_goal_color = "gold";
ide_error_color = "orange";
ide_default_editor = try Sys.getenv "EDITOR" with Not_found -> "editor";
}
......@@ -101,12 +101,12 @@ let load_ide section =
get_bool section ~default:default_ide.ide_show_locs "print_locs";
ide_saving_policy =
get_int section ~default:default_ide.ide_saving_policy "saving_policy";
ide_lighter_location_color =
get_string section ~default:default_ide.ide_lighter_location_color
"lighter_location_color";
ide_location_color =
get_string section ~default:default_ide.ide_location_color
"location_color";
ide_premise_color =
get_string section ~default:default_ide.ide_premise_color
"premise_color";
ide_goal_color =
get_string section ~default:default_ide.ide_goal_color
"goal_color";
ide_error_color =
get_string section ~default:default_ide.ide_error_color
"error_color";
......@@ -146,8 +146,8 @@ let load_config config =
show_labels = ide.ide_show_labels ;
show_locs = ide.ide_show_locs ;
saving_policy = ide.ide_saving_policy ;
lighter_location_color = ide.ide_lighter_location_color;
location_color = ide.ide_location_color;
premise_color = ide.ide_premise_color;
goal_color = ide.ide_goal_color;
error_color = ide.ide_error_color;
max_running_processes = Whyconf.running_provers_max main;
default_editor = ide.ide_default_editor;
......@@ -188,8 +188,8 @@ let save_config t =
let ide = set_bool ide "print_labels" t.show_labels in
let ide = set_bool ide "print_locs" t.show_locs in
let ide = set_int ide "saving_policy" t.saving_policy in
let ide = set_string ide "lighter_location_color" t.lighter_location_color in
let ide = set_string ide "location_color" t.location_color in
let ide = set_string ide "premise_color" t.premise_color in
let ide = set_string ide "goal_color" t.goal_color in
let ide = set_string ide "error_color" t.error_color in
let ide = set_string ide "default_editor" t.default_editor in
let config = set_section config "ide" ide in
......
......@@ -33,8 +33,8 @@ type t =
mutable show_labels : bool;
mutable show_locs : bool;
mutable saving_policy : int;
mutable lighter_location_color : string;
mutable location_color : string;
mutable premise_color : string;
mutable goal_color : string;
mutable error_color : string;
mutable env : Why3.Env.env;
mutable config : Whyconf.config;
......
......@@ -1140,19 +1140,19 @@ let move_to_line ~yalign (v : GSourceView2.source_view) line =
v#scroll_to_mark ~use_align:true ~yalign mark
let lighter_location_tag = source_view#buffer#create_tag
~name:"lighter_location_tag" [`BACKGROUND gconfig.lighter_location_color]
let premise_tag = source_view#buffer#create_tag
~name:"premise_tag" [`BACKGROUND gconfig.premise_color]
let location_tag = source_view#buffer#create_tag
~name:"location_tag" [`BACKGROUND gconfig.location_color]
let goal_tag = source_view#buffer#create_tag
~name:"goal_tag" [`BACKGROUND gconfig.goal_color]
let error_tag = source_view#buffer#create_tag
~name:"error_tag" [`BACKGROUND gconfig.error_color]
let erase_color_loc (v:GSourceView2.source_view) =
let buf = v#buffer in
buf#remove_tag lighter_location_tag ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag location_tag ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag premise_tag ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag goal_tag ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag error_tag ~start:buf#start_iter ~stop:buf#end_iter
let color_loc (v:GSourceView2.source_view) ~color l b e =
......@@ -1198,22 +1198,22 @@ let rec color_locs ~color f =
let rec color_t_locs f =
match f.Term.t_node with
| Term.Tbinop (Term.Timplies,f1,f2) ->
color_locs ~color:lighter_location_tag f1;
color_locs ~color:premise_tag f1;
color_t_locs f2
| Term.Tlet (t,fb) ->
let _,f1 = Term.t_open_bound fb in
color_locs ~color:lighter_location_tag t;
color_locs ~color:premise_tag t;
color_t_locs f1
| Term.Tquant (Term.Tforall,fq) ->
let _,_,f1 = Term.t_open_quant fq in
color_t_locs f1
| _ ->
color_locs ~color:location_tag f
color_locs ~color:goal_tag f
let scroll_to_source_goal g =
let t = M.get_task g in
let id = (Task.task_goal t).Decl.pr_name in
scroll_to_id ~color:location_tag id;
scroll_to_id ~color:goal_tag id;
match t with
| Some
{ Task.task_decl =
......@@ -1226,7 +1226,7 @@ let scroll_to_source_goal g =
let scroll_to_theory th =
let t = M.get_theory th in
let id = t.Theory.th_name in
scroll_to_id ~color:location_tag id
scroll_to_id ~color:goal_tag id
let reload () =
......
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