symbols in (error) messages now consistently with single backslash
authoroheimb
Wed Oct 27 11:15:35 1999 +0200 (1999-10-27)
changeset 7944cc1930ad1a88
parent 7943 e31a3c0c2c1e
child 7945 3aca6352f063
symbols in (error) messages now consistently with single backslash
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Wed Oct 27 11:13:25 1999 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Wed Oct 27 11:15:35 1999 +0200
     1.3 @@ -792,7 +792,7 @@
     1.4        if null toks then Pretty.str "Inner syntax error: unexpected end of input"
     1.5        else
     1.6          Pretty.block (Pretty.str "Inner syntax error at: \"" ::
     1.7 -          Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token)
     1.8 +          Pretty.breaks (map (Pretty.str o str_of_token)
     1.9  		 (rev (tl (rev toks)))) @
    1.10            [Pretty.str "\""]);
    1.11      val expected =
     2.1 --- a/src/Pure/Syntax/syntax.ML	Wed Oct 27 11:13:25 1999 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Oct 27 11:15:35 1999 +0200
     2.3 @@ -353,12 +353,11 @@
     2.4      val chars = Symbol.explode str;
     2.5      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
     2.6  
     2.7 -    fun show_pt pt =
     2.8 -      warning (Symbol.output (Pretty.string_of 
     2.9 -		(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))));
    2.10 +    fun show_pt pt = warning (Pretty.string_of 
    2.11 +			(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
    2.12    in
    2.13      if length pts > ! ambiguity_level then
    2.14 -      (warning ("Ambiguous input " ^ quote (Symbol.output str));
    2.15 +      (warning ("Ambiguous input " ^ quote str);
    2.16         warning "produces the following parse trees:";
    2.17         seq show_pt pts)
    2.18      else ();