src/Pure/Isar/isar_output.ML
changeset 17151 bc97adfeeaa7
parent 17089 f708a31fa8bb
child 17185 5140808111d1
equal deleted inserted replaced
17150:ce2a1aeb42aa 17151:bc97adfeeaa7
   245 
   245 
   246 fun present_span lex default_tags span state state'
   246 fun present_span lex default_tags span state state'
   247     (tag_stack, active_tag, newline, buffer, present_cont) =
   247     (tag_stack, active_tag, newline, buffer, present_cont) =
   248   let
   248   let
   249     val present = fold (fn (raw, tok, d) =>
   249     val present = fold (fn (raw, tok, d) =>
   250       if d > 0 then I
   250       Buffer.add raw o (if d > 0 then I else Buffer.add (output_token lex state' tok)));
   251       else Buffer.add raw #> Buffer.add (output_token lex state' tok));
       
   252 
   251 
   253     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   252     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   254 
   253 
   255     val (tag, tags) = tag_stack;
   254     val (tag, tags) = tag_stack;
   256     val tag' =
   255     val tag' =