# HG changeset patch
# User wenzelm
# Date 1598130708 -7200
# Node ID 16f2288b30cf834a31a4f28a0f5308ad5847f070
# Parent  eef421b724c0589d87555d2f5ea00845fce8b645
avoid odd PIDE markup, notably in kokodi input;

diff -r eef421b724c0 -r 16f2288b30cf src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Aug 22 20:37:31 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Aug 22 23:11:48 2020 +0200
@@ -533,7 +533,7 @@
         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
-                      Print_Mode.setmp [] multiline_string_for_scope scope
+                      multiline_string_for_scope scope
         val kodkod_sat_solver =
           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
diff -r eef421b724c0 -r 16f2288b30cf src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Aug 22 20:37:31 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Aug 22 23:11:48 2020 +0200
@@ -198,8 +198,10 @@
 
 fun multiline_string_for_scope scope =
   let
+    val code_type = Print_Mode.setmp [] o Syntax.string_of_typ o Config.put show_markup false;
+    val code_term = Print_Mode.setmp [] o Syntax.string_of_term o Config.put show_markup false;
     val (primary_cards, secondary_cards, maxes, iters, miscs) =
-      quintuple_for_scope Syntax.string_of_typ Syntax.string_of_term I scope
+      quintuple_for_scope code_type code_term I scope
     val cards = primary_cards @ secondary_cards
   in
     case (if null cards then [] else ["card: " ^ commas (map implode cards)]) @