diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/explore.ml | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | lib/pp.ml | 20 | ||||
| -rw-r--r-- | lib/pp.mli | 4 | ||||
| -rw-r--r-- | lib/pp_diff.ml | 14 |
6 files changed, 23 insertions, 19 deletions
diff --git a/lib/explore.ml b/lib/explore.ml index b3ffef6ac2..139de488e2 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -29,7 +29,7 @@ module Make = functor(S : SearchProblem) -> struct | [i] -> int i | i :: l -> pp_rec l ++ str "." ++ int i in - Feedback.msg_debug (h 0 (pp_rec p) ++ pp) + Feedback.msg_debug (h (pp_rec p) ++ pp) (*s Depth first search. *) diff --git a/lib/flags.ml b/lib/flags.ml index 1d9d6d49bc..83733cf00d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -47,6 +47,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false let debug = ref false +let xml_debug = ref false let in_debugger = ref false let in_toplevel = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 30d1b5b2bd..ebd23a4d20 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -41,6 +41,7 @@ val load_vos_libraries : bool ref (** Debug flags *) val debug : bool ref +val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref @@ -22,7 +22,7 @@ type pp_tag = string type block_type = - | Pp_hbox of int + | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int @@ -131,7 +131,7 @@ let strbrk s = let ismt = function | Ppcmd_empty -> true | _ -> false (* boxing commands *) -let h n s = Ppcmd_box(Pp_hbox n,s) +let h s = Ppcmd_box(Pp_hbox,s) let v n s = Ppcmd_box(Pp_vbox n,s) let hv n s = Ppcmd_box(Pp_hvbox n,s) let hov n s = Ppcmd_box(Pp_hovbox n,s) @@ -151,7 +151,7 @@ let escape_string s = let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring -let quote s = h 0 (str "\"" ++ s ++ str "\"") +let quote s = h (str "\"" ++ s ++ str "\"") let rec pr_com ft s = let (s1,os) = @@ -181,7 +181,7 @@ let split_tag tag = (* pretty printing functions *) let pp_with ft pp = let cpp_open_box = function - | Pp_hbox n -> Format.pp_open_hbox ft () + | Pp_hbox -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n | Pp_hvbox n -> Format.pp_open_hvbox ft n | Pp_hovbox n -> Format.pp_open_hovbox ft n @@ -309,12 +309,14 @@ let db_print_pp fmt pp = let block_type fmt btype = let (bt, v) = match btype with - | Pp_hbox v -> ("Pp_hbox", v) - | Pp_vbox v -> ("Pp_vbox", v) - | Pp_hvbox v -> ("Pp_hvbox", v) - | Pp_hovbox v -> ("Pp_hovbox", v) + | Pp_hbox -> ("Pp_hbox", None) + | Pp_vbox v -> ("Pp_vbox", Some v) + | Pp_hvbox v -> ("Pp_hvbox", Some v) + | Pp_hovbox v -> ("Pp_hovbox", Some v) in - fprintf fmt "%s %d" bt v + match v with + | None -> fprintf fmt "%s" bt + | Some v -> fprintf fmt "%s %d" bt v in let rec db_print_pp_r indent pp = let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in diff --git a/lib/pp.mli b/lib/pp.mli index b265537728..12f1ba9bb2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -43,7 +43,7 @@ type pp_tag = string type t type block_type = - | Pp_hbox of int + | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int @@ -99,7 +99,7 @@ val strbrk : string -> t (** {6 Boxing commands} *) -val h : int -> t -> t +val h : t -> t val v : int -> t -> t val hv : int -> t -> t val hov : int -> t -> t diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml index 988e8e4303..4593bf4b07 100644 --- a/lib/pp_diff.ml +++ b/lib/pp_diff.ml @@ -109,7 +109,7 @@ let shorten_diff_span dtype diff_list = iter 0 len (<) 1; (* left to right *) iter (len-1) (-1) (>) (-1); (* right to left *) - if !changed then Array.to_list diffs else diff_list;; + if !changed then Array.to_list diffs else diff_list let has_changes diffs = let rec has_changes_r diffs added removed = @@ -118,12 +118,12 @@ let has_changes diffs = | `Removed _ :: t -> has_changes_r t added true | h :: t -> has_changes_r t added removed | [] -> (added, removed) in - has_changes_r diffs false false;; + has_changes_r diffs false false (* get the Myers diff of 2 lists of strings *) let diff_strs old_strs new_strs = let diffs = List.rev (StringDiff.diff old_strs new_strs) in - shorten_diff_span `Removed (shorten_diff_span `Added diffs);; + shorten_diff_span `Removed (shorten_diff_span `Added diffs) (* Default string tokenizer. Makes each character a separate strin. Whitespace is not ignored. Doesn't handle UTF-8 differences well. *) @@ -139,7 +139,7 @@ let def_tokenize_string s = let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str = let old_toks = Array.of_list (tokenize_string old_str) and new_toks = Array.of_list (tokenize_string new_str) in - diff_strs old_toks new_toks;; + diff_strs old_toks new_toks let get_dinfo = function | `Common (_, _, s) -> (`Common, s) @@ -281,14 +281,14 @@ let add_diff_tags which pp diffs = skip (); if !diffs <> [] then raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible"); - if has_added || has_removed then wrap_in_bg diff_tag rv else rv;; + if has_added || has_removed then wrap_in_bg diff_tag rv else rv let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp = let open Pp in let o_str = string_of_ppcmds o_pp in let n_str = string_of_ppcmds n_pp in let diffs = diff_str ~tokenize_string o_str n_str in - (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);; + (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs) let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp = let open Pp in @@ -300,4 +300,4 @@ let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false if show_removed && has_removed then let removed = add_diff_tags `Removed o_pp diffs in (v 0 (removed ++ cut() ++ added)) - else added;; + else added |