equal
deleted
inserted
replaced
117 end; |
117 end; |
118 |
118 |
119 |
119 |
120 (* token output *) |
120 (* token output *) |
121 |
121 |
122 val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment; |
|
123 |
|
124 fun output_basic tok = |
122 fun output_basic tok = |
125 let val s = Token.content_of tok in |
123 let val s = Token.content_of tok in |
126 if invisible_token tok then "" |
124 if Token.is_kind Token.Comment tok then "" |
127 else if Token.is_command tok then |
125 else if Token.is_command tok then |
128 "\\isacommand{" ^ output_syms s ^ "}" |
126 "\\isacommand{" ^ output_syms s ^ "}" |
129 else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then |
127 else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then |
130 "\\isakeyword{" ^ output_syms s ^ "}" |
128 "\\isakeyword{" ^ output_syms s ^ "}" |
131 else if Token.is_kind Token.String tok then |
129 else if Token.is_kind Token.String tok then |