Commit 1b3318cf authored by Guillaume Melquiond's avatar Guillaume Melquiond

Create separate "editor" sections to support several Coq editors.

For now, there is no autodetection of the editor. The purpose of this patch
is only to provide the user with sane defaults and to avoid reusing prover
options as editor options. So the user has to manually edit the why3.conf
file to modify a prover/editor association.

Tested with Coqide 8.3 and Proof General 4.1.
parent 37d27ad4
......@@ -270,7 +270,7 @@ version_old = "8.1"
version_old = "8.0"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
editor = "coqide"
[ITP pvs]
name = "PVS"
......@@ -281,3 +281,9 @@ version_ok = "5.0"
command = "@LOCALBIN@why3-cpulimit 0 %m -s proveit %f"
driver = "drivers/pvs.drv"
editor = "pvs %f"
[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
[editor proofgeneral-coq]
command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
......@@ -66,6 +66,17 @@ let load_prover kind (id,section) =
prover_editor = get_string section ~default:"" "editor";
}
let editor_keys =
let add acc k = Sstr.add k acc in
List.fold_left add Sstr.empty
["command"]
let load_editor section =
check_exhaustive section prover_keys;
{ editor_command = get_string section "command";
editor_options = []
}
(** returned in reverse order *)
let load rc =
let atps = get_family rc "ATP" in
......@@ -90,6 +101,19 @@ let provers_found = ref 0
let prover_tips_info = ref false
let read_editors main =
let filename = Filename.concat (Whyconf.datadir main)
"provers-detection-data.conf" in
try
let rc = Rc.from_file filename in
List.fold_left (fun editors (id, section) ->
Meditor.add id (load_editor section) editors
) Meditor.empty (get_family rc "editor")
with
| Failure "lexing" ->
Loc.errorm "Syntax error in provers-detection-data.conf@."
| Not_found ->
Loc.errorm "provers-detection-data.conf not found at %s@." filename
let make_command exec com =
let cmd_regexp = Str.regexp "%\\(.\\)" in
......@@ -207,7 +231,7 @@ let run_auto_detection config =
let detect = List.fold_left (detect_prover main) Mprover.empty l in
let length = Mprover.cardinal detect in
eprintf "%d provers detected.@." length;
set_provers config detect
set_provers (set_editors config (read_editors main)) detect
let list_prover_ids () =
let config = default_config "/dev/null" in
......
......@@ -33,10 +33,11 @@ open Stdlib
- 9 coq realizations
- 10 require %f in editor lines
- 11 change prover identifiers in provers-detection-data.conf
- 12 split editors out of provers
If a configuration doesn't contain the actual magic number we don't use it.*)
let magicnumber = 11
let magicnumber = 12
exception WrongMagicNumber
......@@ -85,14 +86,19 @@ module Prover = struct
2 * Hashtbl.hash s1.prover_name +
3 * Hashtbl.hash s1.prover_version +
5 * Hashtbl.hash s1.prover_altern
end
module Mprover = Map.Make(Prover)
module Sprover = Mprover.Set
module Hprover = Hashtbl.Make(Prover)
module Editor = struct
type t = string
let compare = Pervasives.compare
end
module Meditor = Map.Make(Editor)
(* Configuration file *)
type config_prover = {
......@@ -106,6 +112,11 @@ type config_prover = {
extra_drivers : string list;
}
type config_editor = {
editor_command : string;
editor_options : string list;
}
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
......@@ -174,6 +185,7 @@ type config = {
config : Rc.t;
main : main;
provers : config_prover Mprover.t;
editors : config_editor Meditor.t;
}
let default_main =
......@@ -221,6 +233,16 @@ let set_provers rc provers =
let _,family = Mprover.fold set_prover provers (Sstr.empty,[]) in
set_family rc "prover" family
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 "command" editor.editor_command in
(Sstr.add id ids, (id, section)::family)
let set_editors rc editors =
let _,family = Meditor.fold set_editor editors (Sstr.empty,[]) in
set_family rc "editor" family
let absolute_filename = Sysutil.absolutize_filename
let load_prover dirname provers (id,section) =
......@@ -243,6 +265,12 @@ let load_prover dirname provers (id,section) =
extra_drivers = [];
} provers
let load_editor editors (id, section) =
Meditor.add id
{ editor_command = get_string section "command";
editor_options = [];
} editors
let load_main dirname section =
if get_int ~default:0 section "magic" <> magicnumber then
raise WrongMagicNumber;
......@@ -287,10 +315,13 @@ let get_config (filename,rc) =
in
let provers = get_family rc "prover" in
let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
let editors = get_family rc "editor" in
let editors = List.fold_left load_editor Meditor.empty editors in
{ conf_file = filename;
config = rc;
main = main;
provers = provers;
editors = editors;
}
let default_config conf_file =
......@@ -332,7 +363,17 @@ let merge_config config filename =
with
Not_found -> load_prover dirname provers (id, section)
) config.provers provers in
{ config with main = main; provers = provers }
let editors = get_family rc "editor" in
let editors = List.fold_left
(fun editors (id, section) ->
try
let c = Meditor.find id editors in
let opt = (get_stringl ~default:[] section "option") @ c.editor_options in
Meditor.add id { c with editor_options = opt } editors
with
Not_found -> load_editor editors (id, section)
) config.editors editors in
{ config with main = main; provers = provers; editors = editors }
let save_config config =
let filename = config.conf_file in
......@@ -354,6 +395,12 @@ let set_provers config provers =
provers = provers;
}
let set_editors config editors =
{ config with
config = set_editors config.config editors;
editors = editors;
}
(*******)
let set_conf_file config conf_file = {config with conf_file = conf_file}
......@@ -383,6 +430,8 @@ let () = Exn_printer.register
| e -> raise e
)
let editor_by_id whyconf id =
Meditor.find id whyconf.editors
(******)
......
......@@ -131,6 +131,20 @@ val prover_by_id : config -> string -> config_prover
(** return the configuration of the prover if found, otherwise return
ProverNotFound *)
type config_editor = {
editor_command : string;
editor_options : string list;
}
module Meditor : Stdlib.Map.S with type key = string
val set_editors : config -> config_editor Meditor.t -> config
(** replace the set of editors *)
val editor_by_id : config -> string -> config_editor
(** return the configuration of the editor if found, otherwise return
Not_found *)
(** {2 For accesing other parts of the configuration } *)
(** Access to the Rc.t *)
......
......@@ -824,14 +824,14 @@ let edit_proof eS sched ~default_editor a =
in
let editor =
match npc.prover_config.Whyconf.editor with
| "" -> default_editor
| s ->
String.concat " "(s :: npc.prover_config.Whyconf.extra_options)
| "" -> default_editor
| s ->
try
let ed = Whyconf.editor_by_id eS.whyconf s in
String.concat " "(ed.Whyconf.editor_command ::
ed.Whyconf.editor_options)
with Not_found -> default_editor
in
(*
eprintf "[Editing] goal %s with command %s %s@."
g.Decl.pr_name.id_string editor file;
*)
let file = update_edit_external_proof eS a in
dprintf debug "[Editing] goal %a with command %s %s@."
(fun fmt a -> pp_print_string fmt
......
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