--- a/src/Pure/PIDE/markup.ML Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/PIDE/markup.ML Sun May 24 19:45:42 2020 +0200
@@ -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 scala_functionN: string val scala_function: string -> T
val markupN: string
val consistentN: string
val unbreakableN: string
@@ -405,6 +406,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 (scala_functionN, scala_function) = markup_string "scala_function" nameN;
(* pretty printing *)