plain string output, without funny control chars;
authorwenzelm
Mon, 06 Jul 2015 16:10:00 +0200
changeset 60667 d86c449d30ba
parent 60666 3a0aaf894e21
child 60668 5d281c5fe712
plain string output, without funny control chars;
src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Jul 06 16:03:01 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML	Mon Jul 06 16:10:00 2015 +0200
@@ -49,10 +49,11 @@
 fun pretty_criterion (b, c) =
   let
     fun prfx s = if b then s else "-" ^ s;
+    val show_pat = quote o Input.source_content o Syntax.read_input;
   in
     (case c of
-      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
-    | Loose pat => Pretty.str (prfx (quote pat))
+      Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat)
+    | Loose pat => Pretty.str (prfx (show_pat pat))
     | Name name => Pretty.str (prfx "name: " ^ quote name))
   end;