changeset 62804 | 7b9c5416f30e |
parent 62529 | 8b7bdfc09f3b |
child 64357 | e10fa8afc96c |
--- a/src/Pure/Thy/markdown.ML Fri Apr 01 18:46:25 2016 +0200 +++ b/src/Pure/Thy/markdown.ML Fri Apr 01 18:56:31 2016 +0200 @@ -86,7 +86,7 @@ | (c, pos) :: _ => error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos)); -fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space; +val is_space = Symbol.is_space o Symbol_Pos.symbol; val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false); fun strip_spaces (Antiquote.Text ss :: rest) =