equal
deleted
inserted
replaced
82 |
82 |
83 fun check_blanks source = |
83 fun check_blanks source = |
84 (case bad_blanks source of |
84 (case bad_blanks source of |
85 [] => () |
85 [] => () |
86 | (c, pos) :: _ => |
86 | (c, pos) :: _ => |
87 error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos)); |
87 error ("Bad blank character " ^ quote (ML_Syntax.print_symbol c) ^ Position.here pos)); |
88 |
88 |
89 val is_space = Symbol.is_space o Symbol_Pos.symbol; |
89 val is_space = Symbol.is_space o Symbol_Pos.symbol; |
90 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false); |
90 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false); |
91 |
91 |
92 fun strip_spaces (Antiquote.Text ss :: rest) = |
92 fun strip_spaces (Antiquote.Text ss :: rest) = |