src/Pure/PIDE/markup.ML
changeset 58544 340f130b3d38
parent 58464 5e7fc9974aba
child 58545 30b75b7958d6
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Oct 05 15:05:26 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val position_properties: string list
     1.5    val positionN: string val position: T
     1.6    val expressionN: string val expression: T
     1.7 +  val citationN: string val citation: T
     1.8    val pathN: string val path: string -> T
     1.9    val urlN: string val url: string -> T
    1.10    val indentN: string
    1.11 @@ -346,6 +347,11 @@
    1.12  val (expressionN, expression) = markup_elem "expression";
    1.13  
    1.14  
    1.15 +(* citation *)
    1.16 +
    1.17 +val (citationN, citation) = markup_elem "citation";
    1.18 +
    1.19 +
    1.20  (* external resources *)
    1.21  
    1.22  val (pathN, path) = markup_string "path" nameN;