avoid odd PIDE markup, notably in kokodi input;

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

--- 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)]) @