more robust treatment of Markup.token;

--- a/src/Pure/General/markup.ML	Sat Aug 07 21:03:06 2010 +0200
+++ b/src/Pure/General/markup.ML	Sat Aug 07 21:22:39 2010 +0200
@@ -9,7 +9,7 @@
   type T = string * Properties.T
   val none: T
   val is_none: T -> bool
-  val properties: (string * string) list -> T -> T
+  val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
   val bindingN: string val binding: string -> T
@@ -93,7 +93,7 @@
   val commentN: string val comment: T
   val controlN: string val control: T
   val malformedN: string val malformed: T
-  val tokenN: string val token: T
+  val tokenN: string val token: Properties.T -> T
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
@@ -284,7 +284,8 @@
 val (controlN, control) = markup_elem "control";
 val (malformedN, malformed) = markup_elem "malformed";
 
-val (tokenN, token) = markup_elem "token";
+val tokenN = "token";
+fun token props = (tokenN, props);
 
 val (command_spanN, command_span) = markup_string "command_span" nameN;
 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";

--- a/src/Pure/Isar/token.ML	Sat Aug 07 21:03:06 2010 +0200
+++ b/src/Pure/Isar/token.ML	Sat Aug 07 21:22:39 2010 +0200
@@ -181,7 +181,7 @@
 (* token content *)
 
 fun source_of (Token ((source, (pos, _)), _, _)) =
-  YXML.string_of (XML.Elem ((Markup.tokenN, Position.properties_of pos), [XML.Text source]));
+  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
 
 fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
 

--- a/src/Pure/Syntax/syntax.ML	Sat Aug 07 21:03:06 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Aug 07 21:22:39 2010 +0200
@@ -458,13 +458,15 @@
 (* read token -- with optional YXML encoding of position *)
 
 fun read_token str =
-  let val (text, pos) =
-    (case YXML.parse str handle Fail msg => error msg of
-    (* FIXME avoid literal strings *)
-      XML.Elem (("token", props), [XML.Text text]) => (text, Position.of_properties props)
-    | XML.Elem (("token", props), []) => ("", Position.of_properties props)
-    | XML.Text text => (text, Position.none)
-    | _ => (str, Position.none))
+  let
+    val tree = YXML.parse str handle Fail msg => error msg;
+    val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
+    val pos =
+      (case tree of
+        XML.Elem ((name, props), _) =>
+          if name = Markup.tokenN then Position.of_properties props
+          else Position.none
+      | XML.Text _ => Position.none);
   in (Symbol_Pos.explode (text, pos), pos) end;