equal
deleted
inserted
replaced
116 local |
116 local |
117 |
117 |
118 fun make_span toks = |
118 fun make_span toks = |
119 if not (null toks) andalso Token.is_command (hd toks) then |
119 if not (null toks) andalso Token.is_command (hd toks) then |
120 Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks) |
120 Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks) |
121 else if forall (not o Token.is_proper) toks then Span (Ignored, toks) |
121 else if forall Token.is_improper toks then Span (Ignored, toks) |
122 else Span (Malformed, toks); |
122 else Span (Malformed, toks); |
123 |
123 |
124 fun flush (result, span) = if null span then (result, span) else (rev span :: result, []); |
124 fun flush (result, span) = if null span then (result, span) else (rev span :: result, []); |
125 |
125 |
126 in |
126 in |