equal
deleted
inserted
replaced
113 fun output_basic tok = |
113 fun output_basic tok = |
114 let val s = Token.content_of tok in |
114 let val s = Token.content_of tok in |
115 if invisible_token tok then "" |
115 if invisible_token tok then "" |
116 else if Token.is_command tok then |
116 else if Token.is_command tok then |
117 "\\isacommand{" ^ output_syms s ^ "}" |
117 "\\isacommand{" ^ output_syms s ^ "}" |
118 else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then |
118 else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then |
119 "\\isakeyword{" ^ output_syms s ^ "}" |
119 "\\isakeyword{" ^ output_syms s ^ "}" |
120 else if Token.is_kind Token.String tok then |
120 else if Token.is_kind Token.String tok then |
121 enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) |
121 enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) |
122 else if Token.is_kind Token.AltString tok then |
122 else if Token.is_kind Token.AltString tok then |
123 enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) |
123 enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) |