126 fun check_name is_module s = |
126 fun check_name is_module s = |
127 let |
127 let |
128 val _ = if s = "" then error "Bad empty code name" else (); |
128 val _ = if s = "" then error "Bad empty code name" else (); |
129 val xs = Long_Name.explode s; |
129 val xs = Long_Name.explode s; |
130 val xs' = if is_module |
130 val xs' = if is_module |
131 then map (Name.desymbolize true) xs |
131 then map (Name.desymbolize (SOME true)) xs |
132 else if length xs < 2 |
132 else if length xs < 2 |
133 then error ("Bad code name without module component: " ^ quote s) |
133 then error ("Bad code name without module component: " ^ quote s) |
134 else |
134 else |
135 let |
135 let |
136 val (ys, y) = split_last xs; |
136 val (ys, y) = split_last xs; |
137 val ys' = map (Name.desymbolize true) ys; |
137 val ys' = map (Name.desymbolize (SOME true)) ys; |
138 val y' = Name.desymbolize false y; |
138 val y' = Name.desymbolize (SOME false) y; |
139 in ys' @ [y'] end; |
139 in ys' @ [y'] end; |
140 in if xs' = xs |
140 in if xs' = xs |
141 then if is_module then (xs, "") else split_last xs |
141 then if is_module then (xs, "") else split_last xs |
142 else error ("Invalid code name: " ^ quote s ^ "\n" |
142 else error ("Invalid code name: " ^ quote s ^ "\n" |
143 ^ "better try " ^ quote (Long_Name.implode xs')) |
143 ^ "better try " ^ quote (Long_Name.implode xs')) |