src/Pure/PIDE/markup.ML
changeset 58545 30b75b7958d6
parent 58544 340f130b3d38
child 58850 1bb0ad7827b4
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 17:58:36 2014 +0200
     1.3 @@ -55,7 +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 citationN: string val citation: string -> T
     1.9    val pathN: string val path: string -> T
    1.10    val urlN: string val url: string -> T
    1.11    val indentN: string
    1.12 @@ -349,7 +349,7 @@
    1.13  
    1.14  (* citation *)
    1.15  
    1.16 -val (citationN, citation) = markup_elem "citation";
    1.17 +val (citationN, citation) = markup_string "citation" nameN;
    1.18  
    1.19  
    1.20  (* external resources *)