--- a/src/Pure/PIDE/markup.ML Sun Oct 05 15:05:26 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Sun Oct 05 16:05:17 2014 +0200
@@ -55,6 +55,7 @@
val position_properties: string list
val positionN: string val position: T
val expressionN: string val expression: T
+ val citationN: string val citation: T
val pathN: string val path: string -> T
val urlN: string val url: string -> T
val indentN: string
@@ -346,6 +347,11 @@
val (expressionN, expression) = markup_elem "expression";
+(* citation *)
+
+val (citationN, citation) = markup_elem "citation";
+
+
(* external resources *)
val (pathN, path) = markup_string "path" nameN;