diff options
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r-- | ide/ide_slave.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index dc52ea9a..041f2f83 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -185,13 +185,15 @@ let process_goal sigma g = let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in - let process_hyp d = + let process_hyp d (env,l) = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in - let hyps = - List.map process_hyp - (Termops.compact_named_context_reverse (Environ.named_context env)) in - { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in + (List.fold_right Environ.push_named d' env, + (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in + let (_env, hyps) = + Context.fold_named_list_context process_hyp + (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in + { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } let export_pre_goals pgs = { @@ -289,11 +291,13 @@ let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b | Goptions.IntValue x -> Interface.IntValue x | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s let import_option_value = function | Interface.BoolValue b -> Goptions.BoolValue b | Interface.IntValue x -> Goptions.IntValue x | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s let export_option_state s = { Interface.opt_sync = s.Goptions.opt_sync; @@ -312,6 +316,8 @@ let set_options options = | BoolValue b -> Goptions.set_bool_option_value name b | IntValue i -> Goptions.set_int_option_value name i | StringValue s -> Goptions.set_string_option_value name s + | StringOptValue (Some s) -> Goptions.set_string_option_value name s + | StringOptValue None -> Goptions.unset_option_value_gen None name in List.iter iter options |