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