diff options
Diffstat (limited to 'ide/protocol')
| -rw-r--r-- | ide/protocol/interface.ml | 6 | ||||
| -rw-r--r-- | ide/protocol/richpp.mli | 2 | ||||
| -rw-r--r-- | ide/protocol/xml_printer.mli | 4 | ||||
| -rw-r--r-- | ide/protocol/xmlprotocol.ml | 2 |
4 files changed, 7 insertions, 7 deletions
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) ^ " |- " ^ |