src/Pure/PIDE/markup.ML
changeset 55744 4a4e5686e091
parent 55694 a1184dfb8e00
child 55750 baa7a1e57f4a
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 25 14:56:58 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 25 17:03:55 2014 +0100
     1.3 @@ -97,9 +97,8 @@
     1.4    val document_antiquotation_optionN: string
     1.5    val paragraphN: string val paragraph: T
     1.6    val text_foldN: string val text_fold: T
     1.7 -  val keywordN: string val keyword: T
     1.8 +  val commandN: string
     1.9    val operatorN: string val operator: T
    1.10 -  val commandN: string val command: T
    1.11    val stringN: string val string: T
    1.12    val altstringN: string val altstring: T
    1.13    val verbatimN: string val verbatim: T
    1.14 @@ -396,9 +395,11 @@
    1.15  
    1.16  (* outer syntax *)
    1.17  
    1.18 -val (keywordN, keyword) = markup_elem "keyword";
    1.19 +val commandN = "command";
    1.20 +
    1.21 +val (keyword1N, keyword1) = markup_elem "keyword1";
    1.22 +val (keyword2N, keyword2) = markup_elem "keyword2";
    1.23  val (operatorN, operator) = markup_elem "operator";
    1.24 -val (commandN, command) = markup_elem "command";
    1.25  val (stringN, string) = markup_elem "string";
    1.26  val (altstringN, altstring) = markup_elem "altstring";
    1.27  val (verbatimN, verbatim) = markup_elem "verbatim";
    1.28 @@ -409,9 +410,6 @@
    1.29  val tokenN = "token";
    1.30  fun token props = (tokenN, props);
    1.31  
    1.32 -val (keyword1N, keyword1) = markup_elem "keyword1";
    1.33 -val (keyword2N, keyword2) = markup_elem "keyword2";
    1.34 -
    1.35  
    1.36  (* timing *)
    1.37