# HG changeset patch
# User wenzelm
# Date 1436191800 -7200
# Node ID d86c449d30ba9f13dfa576db426becf7dbd8346b
# Parent  3a0aaf894e21c42fd57c34a419254580a6f57beb
plain string output, without funny control chars;

diff -r 3a0aaf894e21 -r d86c449d30ba 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;