Commit 82e3e856 authored by MARCHE Claude's avatar MARCHE Claude

solve a few issue about proof edition

- use the default editor if no specific editor known
- keep the former result after edition, although obsolete

Note that the "default_editor" setting is moved from the IDE config to
the main config section
parent ebe4a321
......@@ -177,6 +177,8 @@ type main = {
(* plugins to load, without extension, relative to [libdir]/plugins *)
cntexample : bool;
(* true provers should be asked for counter-example model *)
default_editor : string;
(* editor name used when no specific editor known for a prover *)
}
let libdir m =
......@@ -208,6 +210,7 @@ let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let cntexample m = m.cntexample
let default_editor m = m.default_editor
exception StepsCommandNotSpecified of string
......@@ -227,6 +230,8 @@ let set_limits m time mem running =
let set_cntexample m cntexample =
{ m with cntexample = cntexample }
let set_default_editor m e = { m with default_editor = e }
let plugins m = m.plugins
let set_plugins m pl =
(* TODO : sanitize? *)
......@@ -267,6 +272,8 @@ let empty_main =
running_provers_max = 2; (* two provers run in parallel *)
plugins = [];
cntexample = false; (* no counter-examples by default *)
default_editor = (try Sys.getenv "EDITOR" ^ " %f"
with Not_found -> "editor %f");
}
let default_main =
......@@ -286,6 +293,7 @@ let set_main rc main =
set_int section "running_provers_max" main.running_provers_max in
let section = set_stringl section "plugin" main.plugins in
let section = set_bool section "cntexample" main.cntexample in
let section = set_string section "default_editor" main.default_editor in
set_section rc "main" section
exception NonUniqueId
......@@ -517,13 +525,14 @@ let load_main dirname section =
{ libdir = get_string ~default:default_main.libdir section "libdir";
datadir = get_string ~default:default_main.datadir section "datadir";
loadpath = List.map (Sysutil.absolutize_filename dirname)
(get_stringl ~default:[] section "loadpath");
(get_stringl ~default:[] section "loadpath");
timelimit = get_int ~default:default_main.timelimit section "timelimit";
memlimit = get_int ~default:default_main.memlimit section "memlimit";
running_provers_max = get_int ~default:default_main.running_provers_max
section "running_provers_max";
section "running_provers_max";
plugins = get_stringl ~default:[] section "plugin";
cntexample = get_bool ~default:default_main.cntexample section "cntexample"
cntexample = get_bool ~default:default_main.cntexample section "cntexample";
default_editor = get_string ~default:default_main.default_editor section "default_editor";
}
let read_config_rc conf_file =
......
......@@ -81,6 +81,10 @@ val cntexample: main -> bool
val set_limits: main -> int -> int -> int -> main
val set_cntexample: main -> bool -> main
val default_editor: main -> string
(** editor name used when no specific editor known for a prover *)
val set_default_editor: main -> string -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
......
......@@ -37,8 +37,6 @@ type t =
mutable font_size : int;
mutable current_tab : int;
mutable verbose : int;
mutable default_prover : string; (* "" means none *)
mutable default_editor : string;
mutable intro_premises : bool;
mutable show_full_context : bool;
mutable show_labels : bool;
......@@ -88,8 +86,6 @@ type ide = {
ide_goal_color : string;
ide_error_color : string;
ide_iconset : string;
ide_default_prover : string;
ide_default_editor : string;
(* ide_replace_prover : conf_replace_prover; *)
ide_hidden_provers : string list;
}
......@@ -115,10 +111,6 @@ let default_ide =
ide_goal_color = "gold";
ide_error_color = "orange";
ide_iconset = "fatcow";
ide_default_prover = "";
ide_default_editor =
(try Sys.getenv "EDITOR" ^ " %f"
with Not_found -> "editor %f");
ide_hidden_provers = [];
}
......@@ -172,12 +164,6 @@ let load_ide section =
ide_iconset =
get_string section ~default:default_ide.ide_iconset
"iconset";
ide_default_editor =
get_string section ~default:default_ide.ide_default_editor
"default_editor";
ide_default_prover =
get_string section ~default:default_ide.ide_default_prover
"default_prover";
ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
}
......@@ -220,8 +206,6 @@ let load_config config original_config =
goal_color = ide.ide_goal_color;
error_color = ide.ide_error_color;
iconset = ide.ide_iconset;
default_prover = ide.ide_default_prover;
default_editor = ide.ide_default_editor;
config = config;
original_config = original_config;
hidden_provers = ide.ide_hidden_provers;
......@@ -270,9 +254,6 @@ let save_config t =
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 "iconset" t.iconset in
let ide = set_string ide "default_prover" t.default_prover in
let ide = set_string ide "default_editor" t.default_editor in
let ide = set_stringl ide "hidden_prover" t.hidden_provers in
let config = Whyconf.set_section config "ide" ide in
Whyconf.save_config config
......@@ -973,6 +954,7 @@ let provers_page c (notebook:GPack.notebook) =
in ())
(Whyconf.get_provers c.config);
(* default prover *)
(*
let frame2 =
GBin.frame ~label:"Default prover" ~packing:hbox_pack () in
let provers_box =
......@@ -981,9 +963,9 @@ let provers_page c (notebook:GPack.notebook) =
let group =
let b =
GButton.radio_button ~label:"(none)" ~packing:provers_box#add
~active:(c.default_prover = "") () in
~active:(c.config.default_prover = "") () in
let (_ : GtkSignal.id) =
b#connect#toggled ~callback:(fun () -> c.default_prover <- "") in
b#connect#toggled ~callback:(fun () -> c.config.default_prover <- "") in
b#group in
Mprover.iter
(fun _ p ->
......@@ -991,12 +973,13 @@ let provers_page c (notebook:GPack.notebook) =
let label = Pp.string_of_wnl print_prover p.prover in
let b =
GButton.radio_button ~label ~group ~packing:provers_box#add
~active:(name = c.default_prover) () in
~active:(name = c.config.default_prover) () in
let (_ : GtkSignal.id) =
b#connect#toggled ~callback:(fun () -> c.default_prover <- name)
b#connect#toggled ~callback:(fun () -> c.config.default_prover <- name)
in ())
(Whyconf.get_provers c.config)
*)
()
(* Page "Uninstalled provers" *)
......@@ -1056,12 +1039,16 @@ let editors_page c (notebook:GPack.notebook) =
let default_editor_frame =
GBin.frame ~label:"Default editor" ~packing:vbox_pack ()
in
let main = Whyconf.get_main c.config in
let editor_entry =
GEdit.entry ~text:c.default_editor ~packing:default_editor_frame#add ()
GEdit.entry ~text:(default_editor main) ~packing:default_editor_frame#add ()
in
let (_ : GtkSignal.id) =
editor_entry#connect#changed ~callback:
(fun () -> c.default_editor <- editor_entry#text)
editor_entry#connect#changed
~callback:
(fun () ->
c.config <- Whyconf.set_main c.config
(Whyconf.set_default_editor main editor_entry#text))
in
let frame = GBin.frame ~label:"Specific editors" ~packing:vbox_pack () in
let box = GPack.vbox ~border_width:5 ~packing:frame#add () in
......
......@@ -19,8 +19,6 @@ type t =
mutable font_size : int;
mutable current_tab : int;
mutable verbose : int;
mutable default_prover : string;
mutable default_editor : string;
mutable intro_premises : bool;
mutable show_full_context : bool;
mutable show_labels : bool;
......
......@@ -432,15 +432,15 @@ let timeout_handler () =
let q = Queue.create () in
while not (Queue.is_empty prover_tasks_edited) do
(* call is an EditorCall *)
let (_ses,_id,_pr,callback,_started,call,ores) as c =
let (callback,call,ores) as c =
Queue.pop prover_tasks_edited in
let prover_update = Call_provers.query_call call in
match prover_update with
| Call_provers.NoUpdates -> Queue.add c q
| Call_provers.ProverFinished res ->
let res = Opt.fold fuzzy_proof_time res ores in
| Call_provers.ProverFinished _res ->
(* res is meaningless for edition, we returned the old result *)
(* inform the callback *)
callback (Done res)
callback (match ores with None -> Undone | Some r -> Done r)
| _ -> assert (false) (* An edition can only return Noupdates or finished *)
done;
Queue.transfer q prover_tasks_edited;
......@@ -595,6 +595,7 @@ let prepare_edition c ?file pn pr ~notification =
update_goal_node notification session pn;
let pa = get_proof_attempt_node session panid in
let file = Opt.get pa.proof_script in
let old_res = pa.proof_state in
let session_dir = Session_itp.get_dir session in
let file = Filename.concat session_dir file in
let old =
......@@ -616,7 +617,7 @@ let prepare_edition c ?file pn pr ~notification =
Driver.print_task ~cntexample:false ?old driver fmt task;
Opt.iter close_in old;
close_out ch;
panid,file
panid,file,old_res
exception Editor_not_found
......@@ -628,7 +629,7 @@ let schedule_edition c id pr ~callback ~notification =
(* Make sure editor exists. Fails otherwise *)
let editor =
match prover_conf.Whyconf.editor with
| "" -> raise Editor_not_found
| "" -> Whyconf.(default_editor (get_main config))
| s ->
try
let ed = Whyconf.editor_by_id config s in
......@@ -636,7 +637,7 @@ let schedule_edition c id pr ~callback ~notification =
ed.Whyconf.editor_options)
with Not_found -> raise Editor_not_found
in
let panid,file = prepare_edition c id pr ~notification in
let panid,file,old_res = prepare_edition c id pr ~notification in
(* Notification node *)
let callback panid s =
begin
......@@ -663,8 +664,7 @@ let schedule_edition c id pr ~callback ~notification =
editor file;
let call = Call_provers.call_editor ~command:editor file in
callback panid Running;
Queue.add (c.controller_session,id,pr,callback panid,false,call,None)
prover_tasks_edited;
Queue.add (callback panid,call,old_res) prover_tasks_edited;
run_timeout_handler ()
exception TransAlreadyExists of string * string
......
......@@ -223,13 +223,12 @@ val schedule_edition :
val prepare_edition :
controller -> ?file:string -> proofNodeID -> Whyconf.prover ->
(*
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
*)
notification:notifier -> proofAttemptID * string
(** [prepare_edition c id pr filename] prepare for editing the proof
of node [id] with prover [pr], using the file name given. The
editor is not launched. *)
notification:notifier -> proofAttemptID * string * Call_provers.prover_result option
(** [prepare_edition c ?file id pr] prepare for editing the proof of
node [id] with prover [pr]. The editor is not launched. The result
is [(pid,name,res)] where [pid] is the node id the proof_attempt,
[name] is the name of the file to edit, made relative to the
session directory, and [res] is the former result if any. *)
exception TransAlreadyExists of string * string
......
......@@ -1127,9 +1127,8 @@ end
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
let schedule_edition (nid: node_ID) (p: Whyconf.config_prover) =
let schedule_edition (nid: node_ID) (prover: Whyconf.prover) =
let d = get_server_data () in
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
try
let id =
......@@ -1143,8 +1142,8 @@ end
with Not_found ->
P.notify
(Message
(Information
"for edition please select either a goal or a proof attempt"))
(Error
"for edition you must select a proof attempt node"))
(* ----------------- Schedule transformation -------------------- *)
......
......@@ -361,7 +361,7 @@ type command =
| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Edit of Whyconf.config_prover
| Edit of Whyconf.prover
| Bisect
| Replay of bool
| Clean
......@@ -436,7 +436,7 @@ let interp commands_table cont id s =
match parse_prover_name cont.Controller_itp.controller_config cmd args with
| Some (prover_config, limit) ->
if prover_config.Whyconf.interactive then
Edit (prover_config)
Edit prover_config.Whyconf.prover
else
Prove (prover_config, limit)
| None ->
......@@ -451,14 +451,7 @@ let interp commands_table cont id s =
let pa =
Session_itp.get_proof_attempt_node
cont.Controller_itp.controller_session id in
begin try
let p,_ = Whyconf.Hprover.find
cont.Controller_itp.controller_provers
pa.Session_itp.prover in
Edit p
with Not_found ->
QError "cannot edit: uninstalled prover"
end
Edit pa.Session_itp.prover
| _ -> QError ("Please select a proof node in the task tree")
end
| "bisect", _ ->
......
......@@ -64,7 +64,7 @@ type command =
| Transform of string * Trans.gentrans * string list
| Prove of Whyconf.config_prover * Call_provers.resource_limit
| Strategies of string
| Edit of Whyconf.config_prover
| Edit of Whyconf.prover
| Bisect
| Replay of bool
| Clean
......
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