src/Pure/Tools/rail.ML
changeset 61456 b521b8b400f7
parent 59937 6eccb133d4e6
child 61457 3e21699bb83b
equal deleted inserted replaced
61455:0e4c257358cf 61456:b521b8b400f7
   313   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   313   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   314   | vertical_range atom y = (atom, y + 1);
   314   | vertical_range atom y = (atom, y + 1);
   315 
   315 
   316 fun output_rules state rules =
   316 fun output_rules state rules =
   317   let
   317   let
   318     val output_antiq = Thy_Output.eval_antiq state;
   318     val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
   319     fun output_text b s =
   319     fun output_text b s =
   320       Output.output s
   320       Output.output s
   321       |> b ? enclose "\\isakeyword{" "}"
   321       |> b ? enclose "\\isakeyword{" "}"
   322       |> enclose "\\isa{" "}";
   322       |> enclose "\\isa{" "}";
   323 
   323