Add an XML message for "Show Proof Diffs"

Add menu item that uses this

3 files changed, 9 insertions, 7 deletions

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
 
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