59 | hashw_term _ = 0w0 |
59 | hashw_term _ = 0w0 |
60 |
60 |
61 fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
61 fun hash_string s = Word.toInt (hashw_string (s, 0w0)) |
62 val hash_term = Word.toInt o hashw_term |
62 val hash_term = Word.toInt o hashw_term |
63 |
63 |
64 fun strip_c_style_comment _ [] = [] |
|
65 | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = |
|
66 strip_spaces_in_list true is_evil cs |
|
67 | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs |
|
68 and strip_spaces_in_list _ _ [] = [] |
|
69 | strip_spaces_in_list true is_evil (#"%" :: cs) = |
|
70 strip_spaces_in_list true is_evil |
|
71 (cs |> chop_while (not_equal #"\n") |> snd) |
|
72 | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) = |
|
73 strip_c_style_comment is_evil cs |
|
74 | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1] |
|
75 | strip_spaces_in_list skip_comments is_evil [c1, c2] = |
|
76 strip_spaces_in_list skip_comments is_evil [c1] @ |
|
77 strip_spaces_in_list skip_comments is_evil [c2] |
|
78 | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) = |
|
79 if Char.isSpace c1 then |
|
80 strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) |
|
81 else if Char.isSpace c2 then |
|
82 if Char.isSpace c3 then |
|
83 strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs) |
|
84 else |
|
85 str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @ |
|
86 strip_spaces_in_list skip_comments is_evil (c3 :: cs) |
|
87 else |
|
88 str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs) |
|
89 fun strip_spaces skip_comments is_evil = |
64 fun strip_spaces skip_comments is_evil = |
90 implode o strip_spaces_in_list skip_comments is_evil o String.explode |
65 let |
|
66 fun strip_c_style_comment [] accum = accum |
|
67 | strip_c_style_comment (#"*" :: #"/" :: cs) accum = |
|
68 strip_spaces_in_list true cs accum |
|
69 | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum |
|
70 and strip_spaces_in_list _ [] accum = rev accum |
|
71 | strip_spaces_in_list true (#"%" :: cs) accum = |
|
72 strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd) |
|
73 accum |
|
74 | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = |
|
75 strip_c_style_comment cs accum |
|
76 | strip_spaces_in_list _ [c1] accum = |
|
77 accum |> not (Char.isSpace c1) ? cons c1 |
|
78 | strip_spaces_in_list skip_comments (cs as [_, _]) accum = |
|
79 accum |> fold (strip_spaces_in_list skip_comments o single) cs |
|
80 | strip_spaces_in_list skip_comments (c1 :: c2 :: c3 :: cs) accum = |
|
81 if Char.isSpace c1 then |
|
82 strip_spaces_in_list skip_comments (c2 :: c3 :: cs) accum |
|
83 else if Char.isSpace c2 then |
|
84 if Char.isSpace c3 then |
|
85 strip_spaces_in_list skip_comments (c1 :: c3 :: cs) accum |
|
86 else |
|
87 strip_spaces_in_list skip_comments (c3 :: cs) |
|
88 (c1 :: accum |> forall is_evil [c1, c3] ? cons #" ") |
|
89 else |
|
90 strip_spaces_in_list skip_comments (c2 :: c3 :: cs) (cons c1 accum) |
|
91 in |
|
92 String.explode |
|
93 #> rpair [] #-> strip_spaces_in_list skip_comments |
|
94 #> rev #> String.implode |
|
95 end |
91 |
96 |
92 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
97 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
93 val strip_spaces_except_between_idents = strip_spaces true is_ident_char |
98 val strip_spaces_except_between_idents = strip_spaces true is_ident_char |
94 |
99 |
95 val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) |
100 val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) |