equal
deleted
inserted
replaced
56 |
56 |
57 |
57 |
58 fun char_tr (*"_Char"*) [Free (c, _)] = |
58 fun char_tr (*"_Char"*) [Free (c, _)] = |
59 if size c = 1 then mk_char c |
59 if size c = 1 then mk_char c |
60 else error ("Bad character: " ^ quote c) |
60 else error ("Bad character: " ^ quote c) |
61 | char_tr (*"_Char"*) ts = raise_term "char_tr" ts; |
61 | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts); |
62 |
62 |
63 fun char_tr' (*"Char"*) [t1, t2] = |
63 fun char_tr' (*"Char"*) [t1, t2] = |
64 const "_Char" $ free (ssquote (dest_nibs t1 t2)) |
64 const "_Char" $ free (ssquote (dest_nibs t1 t2)) |
65 | char_tr' (*"Char"*) _ = raise Match; |
65 | char_tr' (*"Char"*) _ = raise Match; |
66 |
66 |
75 | dest_string _ = raise Match; |
75 | dest_string _ = raise Match; |
76 |
76 |
77 |
77 |
78 fun string_tr (*"_String"*) [Free (txt, _)] = |
78 fun string_tr (*"_String"*) [Free (txt, _)] = |
79 mk_string (map mk_char (explode txt)) |
79 mk_string (map mk_char (explode txt)) |
80 | string_tr (*"_String"*) ts = raise_term "string_tr" ts; |
80 | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts); |
81 |
81 |
82 fun cons_tr' (*"op #"*) [c, cs] = |
82 fun cons_tr' (*"op #"*) [c, cs] = |
83 const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs))) |
83 const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs))) |
84 | cons_tr' (*"op #"*) ts = raise Match; |
84 | cons_tr' (*"op #"*) ts = raise Match; |
85 |
85 |