Fixing typos - Part 2

5 files changed, 8 insertions, 8 deletions

diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml
index 251e3dded3..4c66a6944e 100644
--- a/ide/configwin_types.ml
+++ b/ide/configwin_types.ml
@@ -87,7 +87,7 @@ type modifiers_param = {
              (** The value, as a list of modifiers and a key code *)
     md_editable : bool ; (** indicates if the value can be changed *)
     md_f_apply : Gdk.Tags.modifier list -> unit ;
-             (** the function to call to apply the new value of the paramter *)
+             (** the function to call to apply the new value of the parameter *)
     md_help : string option ; (** optional help string *)
     md_expand : bool ; (** expand or not *)
     md_allow : Gdk.Tags.modifier list
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index ccb6bedaf6..9d8fdf6335 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -34,7 +34,7 @@ type status = {
   status_path : string list;
   (** Module path of the current proof *)
   status_proofname : string option;
-  (** Current proof name. [None] if no focussed proof is in progress *)
+  (** Current proof name. [None] if no focused proof is in progress *)
   status_allproofs : string list;
   (** List of all pending proofs. Order is not significant *)
   status_proofnum : int;
@@ -43,7 +43,7 @@ type status = {
 
 type 'a pre_goals = {
   fg_goals : 'a list;
-  (** List of the focussed goals *)
+  (** List of the focused goals *)
   bg_goals : ('a list * 'a list) list;
   (** Zipper representing the unfocused background goals *)
   shelved_goals : 'a list;
@@ -70,7 +70,7 @@ type option_state = {
   opt_sync  : bool;
   (** Whether an option is synchronous *)
   opt_depr  : bool;
-  (** Wheter an option is deprecated *)
+  (** Whether an option is deprecated *)
   opt_name  : string;
   (** A short string that is displayed when using [Test] *)
   opt_value : option_value;
diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f1..18d4b1eeee 100644
--- a/ide/protocol/richpp.mli
+++ b/ide/protocol/richpp.mli
@@ -25,7 +25,7 @@ type 'annotation located = {
     of [ppcmds] as a semi-structured document
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
-    annotation. [width] sets the printing witdh of the formatter. *)
+    annotation. [width] sets the printing width of the formatter. *)
 val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c808f..4b47aa9f7c 100644
--- a/ide/protocol/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
@@ -16,11 +16,11 @@ type target = TChannel of out_channel | TBuffer of Buffer.t
 val make : target -> t
 
 (** Print the xml data structure to a source into a compact xml string (without
- any user-readable formating ). *)
+ any user-readable formatting ). *)
 val print : t -> xml -> unit
 
 (** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
+ any user-readable formatting ). *)
 val to_string : xml -> string
 
 (** Print the xml data structure into an user-readable string with
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210f..5b37ca35ed 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -405,7 +405,7 @@ end = struct
           | (lg, rg) :: l ->
             Printf.sprintf "%i:%a"
               (List.length lg + List.length rg) pr_focus l in
-        Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+        Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals
     else
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
         "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^