diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 23 | ||||
| -rw-r--r-- | ide/utils/config_file.ml | 3 |
2 files changed, 12 insertions, 14 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bb8723dfe6..4171eb20de 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,6 +13,10 @@ open Util open Pp open Printer +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration + (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered when the -ideslave option is passed to Coqtop. Currently CoqIDE is @@ -96,7 +100,7 @@ let is_undo cmd = match cmd with (** Check whether a command is forbidden by CoqIDE *) let coqide_cmd_checks (loc,ast) = - let user_error s = CErrors.user_err_loc (loc, "CoqIde", str s) in + let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then @@ -133,7 +137,8 @@ let annotate phrase = (** Goal display *) let hyp_next_tac sigma env decl = - let (id,_,ast) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in + let ast = NamedDecl.get_type decl in let id_s = Names.Id.to_string id in let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ @@ -190,16 +195,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in - let d' = List.map (fun name -> let open Context.Named.Declaration in - match pi2 d with - | None -> LocalAssum (name, pi3 d) - | Some value -> LocalDef (name, value, pi3 d)) - (pi1 d) in + let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, - (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in + (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in let (_env, hyps) = - Context.NamedList.fold process_hyp + Context.Compacted.fold 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; } @@ -300,7 +301,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - CErrors.errorlabstrm "Search.interface_search" + CErrors.user_err ~hdr:"Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 4d0aabeb6a..e4c613913b 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -44,9 +44,6 @@ (* ******************************************************************************** *) (* This code is intended to be usable without any dependencies. *) -(* pipeline style, see for instance Raw.of_channel. *) -let (|>) x f = f x - (* as List.assoc, but applies f to the element matching [key] and returns the list where this element has been replaced by the result of f. *) let rec list_assoc_remove key f = function |