# HG changeset patch
# User wenzelm
# Date 1459529791 -7200
# Node ID 7b9c5416f30edef859076002bbc586bd5e6efb6c
# Parent  5f73bf6ba98bcddd52997a5119f5ea82a8e83cb1
tuned signature;

diff -r 5f73bf6ba98b -r 7b9c5416f30e src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Apr 01 18:46:25 2016 +0200
+++ b/src/Pure/General/symbol.ML	Fri Apr 01 18:56:31 2016 +0200
@@ -13,6 +13,7 @@
   val open_: symbol
   val close: symbol
   val space: symbol
+  val is_space: symbol -> bool
   val comment: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
@@ -99,6 +100,7 @@
 val close = "\<close>";
 
 val space = chr 32;
+fun is_space s = s = space;
 
 local
   val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
diff -r 5f73bf6ba98b -r 7b9c5416f30e src/Pure/Thy/markdown.ML
--- 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) =