src/Pure/Thy/latex.ML
changeset 11012 8eb472444705
parent 10955 36741b4fe109
child 11719 49c14348a42b
equal deleted inserted replaced
11011:14b78c0c9f05 11012:8eb472444705
    90   Verbatim;
    90   Verbatim;
    91 
    91 
    92 
    92 
    93 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    93 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    94 
    94 
    95 fun strip_blanks s =
       
    96   implode (#1 (Library.take_suffix Symbol.is_blank
       
    97     (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
       
    98 
       
    99 fun output_tok (Basic tok, _) =
    95 fun output_tok (Basic tok, _) =
   100       let val s = T.val_of tok in
    96       let val s = T.val_of tok in
   101         if invisible_token tok then ""
    97         if invisible_token tok then ""
   102         else if T.is_kind T.Command tok then
    98         else if T.is_kind T.Command tok then
   103           "\\isacommand{" ^ output_syms s ^ "}"
    99           "\\isacommand{" ^ output_syms s ^ "}"
   105           "\\isakeyword{" ^ output_syms s ^ "}"
   101           "\\isakeyword{" ^ output_syms s ^ "}"
   106         else if T.is_kind T.String tok then output_syms (quote s)
   102         else if T.is_kind T.String tok then output_syms (quote s)
   107         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
   103         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
   108         else output_syms s
   104         else output_syms s
   109       end
   105       end
   110   | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
   106   | output_tok (Markup cmd, txt) =
       
   107       "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"
   111   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   108   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   112       strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   109       Symbol.strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   113   | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";
   110   | output_tok (Verbatim, txt) = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
   114 
   111 
   115 
   112 
   116 val output_tokens = implode o map output_tok;
   113 val output_tokens = implode o map output_tok;
   117 
   114 
   118 
   115