markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);

--- a/src/Pure/General/symbol_pos.ML	Sat May 26 22:12:18 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun May 27 13:42:01 2018 +0200
@@ -40,6 +40,7 @@
   type text = string
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
+  val explode_delete: text * Position.T -> T list * Position.T list
   val explode: text * Position.T -> T list
   val explode0: string -> T list
   val scan_ident: T list scanner
@@ -253,13 +254,17 @@
   let val syms' = (("", pos1) :: syms @ [("", pos2)])
   in (implode syms', range syms') end;
 
-fun explode (str, pos) =
+fun explode_delete (str, pos) =
   let
     val (res, _) =
       fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
         (Symbol.explode str) ([], Position.no_range_position pos);
-  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
+  in
+    fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
+      res ([], [])
+  end;
 
+val explode = explode_delete #> #1;
 fun explode0 str = explode (str, Position.none);
 
 

--- a/src/Pure/Isar/token.ML	Sat May 26 22:12:18 2018 +0100
+++ b/src/Pure/Isar/token.ML	Sun May 27 13:42:01 2018 +0200
@@ -54,6 +54,7 @@
   val is_blank: T -> bool
   val is_newline: T -> bool
   val content_of: T -> string
+  val source_of: T -> string
   val input_of: T -> Input.source
   val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
@@ -266,6 +267,7 @@
 (* token content *)
 
 fun content_of (Token (_, (_, x), _)) = x;
+fun source_of (Token ((source, _), _, _)) = source;
 
 fun input_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
@@ -318,8 +320,11 @@
     keyword_reports tok
       [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)]
   else
-    let val (m, text) = token_kind_markup (kind_of tok)
-    in [((pos_of tok, m), text)] end;
+    let
+      val pos = pos_of tok;
+      val (m, text) = token_kind_markup (kind_of tok);
+      val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
+    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end;
 
 fun markups keywords = map (#2 o #1) o reports keywords;
 

--- a/src/Pure/PIDE/markup.ML	Sat May 26 22:12:18 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun May 27 13:42:01 2018 +0200
@@ -73,6 +73,7 @@
   val wordsN: string val words: T
   val no_wordsN: string val no_words: T
   val hiddenN: string val hidden: T
+  val deleteN: string val delete: T
   val system_optionN: string
   val sessionN: string
   val theoryN: string
@@ -402,6 +403,8 @@
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
+val (deleteN, delete) = markup_elem "delete";
+
 
 (* misc entities *)
 

--- a/src/Pure/PIDE/markup.scala	Sat May 26 22:12:18 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun May 27 13:42:01 2018 +0200
@@ -242,6 +242,8 @@
 
   val HIDDEN = "hidden"
 
+  val DELETE = "delete"
+
 
   /* misc entities */