aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/xmlprotocol.ml3
2 files changed, 3 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1b4c5d3be0..4a1d688f51 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -166,7 +166,7 @@ let flags_to_color f =
else `NAME Preferences.processed_color#get
(* Move to utils? *)
-let rec validate (s : Pp.std_ppcmds) = match s with
+let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with
| Pp.Ppcmd_empty
| Pp.Ppcmd_print_break _
| Pp.Ppcmd_force_newline -> true
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index b4f2ad0bef..5f80d68974 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -110,7 +110,7 @@ let to_box = let open Pp in
| x -> raise (Marshal_error("*ppbox",PCData x))
)
-let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with
+let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
| Ppcmd_empty -> constructor "ppdoc" "emtpy" []
| Ppcmd_string s -> constructor "ppdoc" "string" [of_string s]
| Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl]
@@ -123,6 +123,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with
let rec to_pp xpp = let open Pp in
+ Pp.unrepr @@
do_match "ppdoc" (fun s args -> match s with
| "empty" -> Ppcmd_empty
| "string" -> Ppcmd_string (to_string (singleton args))