src/Pure/Thy/thy_output.ML
changeset 67357 d7c6054b2ab1
parent 67356 ba226b87c69e
child 67358 dfee70a24f0c
equal deleted inserted replaced
67356:ba226b87c69e 67357:d7c6054b2ab1
   244   end;
   244   end;
   245 
   245 
   246 
   246 
   247 (* output tokens with comments *)
   247 (* output tokens with comments *)
   248 
   248 
   249 fun output_markup state cmd source =
       
   250   Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
       
   251     (output_text state {markdown = false} source);
       
   252 
       
   253 local
   249 local
   254 
   250 
   255 fun output_symbols syms =
   251 fun output_symbols syms =
   256   [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
   252   [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
   257 
   253 
   258 fun output_symbols_comment state (is_comment, syms) =
   254 fun output_symbols_comment state (is_comment, syms) =
   259   if is_comment then
   255   if is_comment then
   260     output_markup state "cmt"
   256     Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
   261       (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms))
   257       (output_text state {markdown = false}
       
   258         (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
   262   else output_symbols syms;
   259   else output_symbols syms;
   263 
   260 
   264 val scan_symbols_comment =
   261 val scan_symbols_comment =
   265   Scan.many1 (fn (s, _) => s <> Symbol.comment andalso Symbol.not_eof s) >> pair false ||
   262   Scan.many1 (fn (s, _) => s <> Symbol.comment andalso Symbol.not_eof s) >> pair false ||
   266   (Symbol_Pos.$$ Symbol.comment ::: Scan.many (Symbol.is_blank o Symbol_Pos.symbol)) --
   263   (Symbol_Pos.$$ Symbol.comment ::: Scan.many (Symbol.is_blank o Symbol_Pos.symbol)) --
   336 
   333 
   337 fun present_token state tok =
   334 fun present_token state tok =
   338   (case tok of
   335   (case tok of
   339     No_Token => []
   336     No_Token => []
   340   | Basic_Token tok => output_token state tok
   337   | Basic_Token tok => output_token state tok
   341   | Markup_Token (cmd, source) => output_markup state cmd source
   338   | Markup_Token (cmd, source) =>
       
   339       Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
       
   340         (output_text state {markdown = false} source)
   342   | Markup_Env_Token (cmd, source) =>
   341   | Markup_Env_Token (cmd, source) =>
   343       [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
   342       [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
   344   | Raw_Token source =>
   343   | Raw_Token source =>
   345       Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
   344       Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
   346 
   345