src/Pure/PIDE/markup.ML
changeset 55763 4b3907cb5654
parent 55761 213b9811f59f
child 55828 42ac3cfb89f6
equal deleted inserted replaced
55762:27a45aec67a0 55763:4b3907cb5654
   107   val commentN: string val comment: T
   107   val commentN: string val comment: T
   108   val controlN: string val control: T
   108   val controlN: string val control: T
   109   val tokenN: string val token: Properties.T -> T
   109   val tokenN: string val token: Properties.T -> T
   110   val keyword1N: string val keyword1: T
   110   val keyword1N: string val keyword1: T
   111   val keyword2N: string val keyword2: T
   111   val keyword2N: string val keyword2: T
       
   112   val keyword3N: string val keyword3: T
   112   val elapsedN: string
   113   val elapsedN: string
   113   val cpuN: string
   114   val cpuN: string
   114   val gcN: string
   115   val gcN: string
   115   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   116   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   116   val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   117   val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   398 (* outer syntax *)
   399 (* outer syntax *)
   399 
   400 
   400 val (commandN, command) = markup_elem "command";
   401 val (commandN, command) = markup_elem "command";
   401 val (keyword1N, keyword1) = markup_elem "keyword1";
   402 val (keyword1N, keyword1) = markup_elem "keyword1";
   402 val (keyword2N, keyword2) = markup_elem "keyword2";
   403 val (keyword2N, keyword2) = markup_elem "keyword2";
       
   404 val (keyword3N, keyword3) = markup_elem "keyword3";
   403 val (operatorN, operator) = markup_elem "operator";
   405 val (operatorN, operator) = markup_elem "operator";
   404 val (stringN, string) = markup_elem "string";
   406 val (stringN, string) = markup_elem "string";
   405 val (altstringN, altstring) = markup_elem "altstring";
   407 val (altstringN, altstring) = markup_elem "altstring";
   406 val (verbatimN, verbatim) = markup_elem "verbatim";
   408 val (verbatimN, verbatim) = markup_elem "verbatim";
   407 val (cartoucheN, cartouche) = markup_elem "cartouche";
   409 val (cartoucheN, cartouche) = markup_elem "cartouche";