Commit 0fb98676 authored by MARCHE Claude's avatar MARCHE Claude

Pretty names for editors

parent 630b8d50
......@@ -309,10 +309,13 @@ editor = "coqide"
# command = "pvs %f"
[editor coqide]
name = "CoqIDE"
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
[editor proofgeneral-coq]
name = "Emacs/ProofGeneral/Coq"
command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
[editor altgr-ergo]
name = "AltGr-Ergo"
command = "altgr-ergo %f"
......@@ -74,7 +74,8 @@ let editor_keys =
let load_editor section =
check_exhaustive section prover_keys;
{ editor_command = get_string section "command";
{ editor_name = get_string section "name";
editor_command = get_string section "command";
editor_options = []
}
......
......@@ -120,6 +120,7 @@ type config_prover = {
}
type config_editor = {
editor_name : string;
editor_command : string;
editor_options : string list;
}
......@@ -244,6 +245,7 @@ let set_provers rc provers =
let set_editor id editor (ids, family) =
if Sstr.mem id ids then raise NonUniqueId;
let section = empty_section in
let section = set_string section "name" editor.editor_name in
let section = set_string section "command" editor.editor_command in
(Sstr.add id ids, (id, section)::family)
......@@ -304,7 +306,8 @@ let load_prover dirname provers (id,section) =
let load_editor editors (id, section) =
Meditor.add id
{ editor_command = get_string section "command";
{ editor_name = get_string ~default:id section "name";
editor_command = get_string section "command";
editor_options = [];
} editors
......
......@@ -133,6 +133,7 @@ val prover_by_id : config -> string -> config_prover
ProverNotFound *)
type config_editor = {
editor_name : string;
editor_command : string;
editor_options : string list;
}
......
......@@ -728,12 +728,14 @@ let editors_page c (notebook:GPack.notebook) =
let frame = GBin.frame ~label:"Specific editors" ~packing:page#pack () in
let box = GPack.vbox ~border_width:5 ~packing:frame#add () in
let editors = Whyconf.get_editors c.config in
let _,strings,indexes =
let _,strings,indexes,map =
Meditor.fold
(fun k _ (i,str,ind) -> (i+1,k::str,Meditor.add k i ind))
editors (2, [], Meditor.empty)
(fun k data (i,str,ind,map) ->
let n = data.editor_name in
(i+1, n::str, Meditor.add k i ind, Meditor.add n k map))
editors (2, [], Meditor.empty, Meditor.empty)
in
let strings = "default" :: "--" :: (List.rev strings) in
let strings = "(default)" :: "--" :: (List.rev strings) in
let add_prover p pi =
let text = p.prover_name ^ " " ^ p.prover_version in
let hb = GPack.hbox ~homogeneous:false ~packing:box#pack () in
......@@ -754,8 +756,10 @@ let editors_page c (notebook:GPack.notebook) =
| Some row ->
let data =
match combo#model#get ~row ~column with
| "default" -> ""
| s -> s
| "(default)" -> ""
| s ->
try Meditor.find s map
with Not_found -> assert false
in
(* Format.eprintf "prover %a : selected editor '%s'@." *)
(* print_prover p data; *)
......
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