230 local |
230 local |
231 |
231 |
232 fun err_bad_nesting pos = |
232 fun err_bad_nesting pos = |
233 error ("Bad nesting of commands in presentation" ^ pos); |
233 error ("Bad nesting of commands in presentation" ^ pos); |
234 |
234 |
235 fun edge1 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else x)); |
235 fun edge which f (x: string option, y) = |
236 fun edge2 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else y)); |
236 if x = y then I |
237 |
237 else (case which (x, y) of NONE => I | SOME txt => Buffer.add txt); |
238 val begin_tag = edge2 Latex.begin_tag; |
238 |
239 val end_tag = edge1 Latex.end_tag; |
239 val begin_tag = edge #2 Latex.begin_tag; |
240 fun open_delim delim e = edge2 Latex.begin_delim e #> delim #> edge2 Latex.end_delim e; |
240 val end_tag = edge #1 Latex.end_tag; |
241 fun close_delim delim e = edge1 Latex.begin_delim e #> delim #> edge1 Latex.end_delim e; |
241 fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; |
|
242 fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; |
242 |
243 |
243 in |
244 in |
244 |
245 |
245 fun present_span lex default_tags span state state' |
246 fun present_span lex default_tags span state state' |
246 (tag_stack, active_tag, newline, buffer, present_cont) = |
247 (tag_stack, active_tag, newline, buffer, present_cont) = |