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 */