diff -r d9a54c4c9da9 -r 3cc73d00553c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 28 21:56:24 2020 +0100
@@ -68,6 +68,7 @@
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
+  val toolN: string val tool: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
@@ -403,6 +404,7 @@
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
+val (toolN, tool) = markup_string "tool" nameN;
 
 
 (* pretty printing *)