src/Pure/Isar/token.ML

   val is_error: T -> bool
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
   val inner_syntax_of: T -> string
-  val source_position_of: T -> Symbol_Pos.text * Position.T
+  val source_position_of: T -> Symbol_Pos.source
   val content_of: T -> string
   val markup: T -> Markup.T * string
   val unparse: T -> string
   val print: T -> string
   val text_of: T -> string * string

   | InternalValue => "internal value"
   | Error _ => "bad input"
   | Sync => "sync marker"
   | EOF => "end-of-input";
 
+val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
+
 
 (* position *)
 
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;

   | is_newline _ = false;
 
 
 (* token content *)
 
-fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
+fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) =
   if YXML.detect x then x
-  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
-
-fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
+  else
+    let
+      val delimited = delimited_kind kind;
+      val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
+    in YXML.string_of tree end;
+
+fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
+  {delimited = delimited_kind kind, text = source, pos = pos};
 
 fun content_of (Token (_, (_, x), _)) = x;
 
 
 (* markup *)