src/Pure/Thy/latex.ML
changeset 27809 a1e409db516b
parent 27781 5a82ee34e9fc
child 27874 f0364f1c0ecf
equal deleted inserted replaced
27808:4dd3d5efcc7f 27809:a1e409db516b
   105 structure T = OuterLex;
   105 structure T = OuterLex;
   106 
   106 
   107 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
   107 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
   108 
   108 
   109 fun output_basic tok =
   109 fun output_basic tok =
   110   let val s = T.val_of tok in
   110   let val s = T.content_of tok in
   111     if invisible_token tok then ""
   111     if invisible_token tok then ""
   112     else if T.is_kind T.Command tok then
   112     else if T.is_kind T.Command tok then
   113       "\\isacommand{" ^ output_syms s ^ "}"
   113       "\\isacommand{" ^ output_syms s ^ "}"
   114     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
   114     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
   115       "\\isakeyword{" ^ output_syms s ^ "}"
   115       "\\isakeyword{" ^ output_syms s ^ "}"