merged

--- a/src/HOL/Library/case_converter.ML	Sun May 27 22:56:43 2018 +0100
+++ b/src/HOL/Library/case_converter.ML	Sun May 27 22:57:06 2018 +0100
@@ -15,9 +15,6 @@
     if eq (k, k') then (SOME (k', v), kvs)
     else apsnd (cons (k', v)) (lookup_remove eq k kvs)
 
-fun map_option _ NONE = NONE
-  | map_option f (SOME x) = SOME (f x)
-
 fun mk_abort msg t =
   let 
     val T = fastype_of t
@@ -72,7 +69,7 @@
       then SOME (End (body_type T))
       else
         let
-          fun f (i, t) = term_to_coordinates P t |> map_option (pair i)
+          fun f (i, t) = term_to_coordinates P t |> Option.map (pair i)
           val tcos = map_filter I (map_index f args)
         in
           if null tcos then NONE
@@ -474,7 +471,7 @@
     val (typ_list, poss) = lhss
       |> Ctr_Sugar_Util.transpose
       |> map_index to_coordinates
-      |> map_filter (map_option add_T)
+      |> map_filter (Option.map add_T)
       |> flat
       |> split_list 
   in

--- a/src/Pure/General/symbol_pos.ML	Sun May 27 22:56:43 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun May 27 22:57:06 2018 +0100
@@ -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	Sun May 27 22:56:43 2018 +0100
+++ b/src/Pure/Isar/token.ML	Sun May 27 22:57:06 2018 +0100
@@ -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/document.scala	Sun May 27 22:56:43 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Sun May 27 22:57:06 2018 +0100
@@ -358,14 +358,14 @@
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
 
-    def is_hidden(name: Node.Name): Boolean =
+    def is_suppressed(name: Node.Name): Boolean =
     {
       val graph1 = graph.default_node(name, Node.empty)
       graph1.is_maximal(name) && graph1.get_node(name).is_empty
     }
 
-    def purge(pred: Node.Name => Boolean): Option[Nodes] =
-      graph.keys_iterator.filter(pred).toList match {
+    def purge_suppressed: Option[Nodes] =
+      graph.keys_iterator.filter(is_suppressed(_)).toList match {
         case Nil => None
         case del => Some(new Nodes((graph /: del)(_.del_node(_))))
       }
@@ -409,10 +409,6 @@
     val init: Version = new Version()
     def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
 
-    def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
-      : Map[Document_ID.Version, Version] =
-      (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
-
     def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version])
       : Future[Version] =
     {
@@ -425,6 +421,13 @@
       }
       else future
     }
+
+    def purge_suppressed(
+      versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] =
+    {
+      (versions /:
+        (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _)
+    }
   }
 
   final class Version private(
@@ -433,12 +436,8 @@
   {
     override def toString: String = "Version(" + id + ")"
 
-    def purge_hidden: Option[Version] =
-      nodes.purge(nodes.is_hidden(_)).map(new Version(id, _))
-
-    def purge_blobs(blobs: Set[Node.Name]): Option[Version] =
-      nodes.purge(name => nodes(name).get_blob.isDefined && !blobs.contains(name)).
-        map(new Version(id, _))
+    def purge_suppressed: Option[Version] =
+      nodes.purge_suppressed.map(new Version(id, _))
   }
 
 
@@ -807,7 +806,7 @@
 
     def removed_versions(removed: List[Document_ID.Version]): State =
     {
-      val versions1 = Version.purge(_.purge_hidden, versions -- removed)
+      val versions1 = Version.purge_suppressed(versions -- removed)
 
       val assignments1 = assignments -- removed
       var blobs1_names = Set.empty[Node.Name]
@@ -834,16 +833,14 @@
         }
       }
 
-      val versions2 = Version.purge(_.purge_blobs(blobs1_names), versions1)
-
       copy(
-        versions = versions2,
+        versions = versions1,
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
         assignments = assignments1,
-        history = history.purge(versions2),
+        history = history.purge(versions1),
         removing_versions = false)
     }
 

--- a/src/Pure/PIDE/markup.ML	Sun May 27 22:56:43 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun May 27 22:57:06 2018 +0100
@@ -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	Sun May 27 22:56:43 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun May 27 22:57:06 2018 +0100
@@ -242,6 +242,8 @@
 
   val HIDDEN = "hidden"
 
+  val DELETE = "delete"
+
 
   /* misc entities */
 

--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun May 27 22:56:43 2018 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sun May 27 22:57:06 2018 +0100
@@ -245,7 +245,7 @@
       })
 
     val nodes_status2 =
-      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
+      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))
 
     if (nodes_status != nodes_status2) {
       nodes_status = nodes_status2