equal
deleted
inserted
replaced
67 |
67 |
68 fun output_sym s = |
68 fun output_sym s = |
69 if size s = 1 then output_chr s |
69 if size s = 1 then output_chr s |
70 else |
70 else |
71 (case explode s of |
71 (case explode s of |
72 "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " " |
72 "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) ^ " " |
|
73 | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " " |
73 | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}" |
74 | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}" |
74 | _ => sys_error "output_sym"); |
75 | _ => sys_error "output_sym"); |
75 |
76 |
76 in |
77 in |
77 |
78 |