src/Pure/Isar/token.ML
changeset 43773 e8ba493027a3
parent 43731 70072780e095
child 43947 9b00f09f7721
equal deleted inserted replaced
43772:c825594fd0c1 43773:e8ba493027a3
   189 fun content_of (Token (_, (_, x), _)) = x;
   189 fun content_of (Token (_, (_, x), _)) = x;
   190 
   190 
   191 
   191 
   192 (* unparse *)
   192 (* unparse *)
   193 
   193 
   194 fun escape q =
       
   195   implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
       
   196 
       
   197 fun unparse (Token (_, (kind, x), _)) =
   194 fun unparse (Token (_, (kind, x), _)) =
   198   (case kind of
   195   (case kind of
   199     String => x |> quote o escape "\""
   196     String => Symbol_Pos.quote_string_qq x
   200   | AltString => x |> enclose "`" "`" o escape "`"
   197   | AltString => Symbol_Pos.quote_string_bq x
   201   | Verbatim => x |> enclose "{*" "*}"
   198   | Verbatim => enclose "{*" "*}" x
   202   | Comment => x |> enclose "(*" "*)"
   199   | Comment => enclose "(*" "*)" x
   203   | Sync => ""
   200   | Sync => ""
   204   | EOF => ""
   201   | EOF => ""
   205   | _ => x);
   202   | _ => x);
   206 
   203 
   207 fun text_of tok =
   204 fun text_of tok =