345 *}

   345 *}

   346 

   346 

   347 section {* Parsing Theory Syntax *}

   347 section {* Parsing Theory Syntax *}

   348 

   348 

   349 text {*

   349 text {*

   350   Most of the time, however, Isabelle developers have to deal with parsing

   352   Most of the time, however, Isabelle developers have to deal with parsing

   351   tokens, not strings.  These token parsers have the type:

   353   tokens, not strings.  These token parsers have the type:

   352 *}

   354 *}

   353   

   355   

   354 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}

   356 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}

   710 *}

   712 *}

   711 

   713 

   712 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   714 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   713 

   715 

   714 text {*

   716 text {*

   715   Often new commands, for example for providing new definitional principles,

   719   Often new commands, for example for providing new definitional principles,

   716   need to be implemented. While this is not difficult on the ML-level,

   720   need to be implemented. While this is not difficult on the ML-level,

   717   new commands, in order to be useful, need to be recognised by

   721   new commands, in order to be useful, need to be recognised by

   718   ProofGeneral. This results in some subtle configuration issues, which we

   722   ProofGeneral. This results in some subtle configuration issues, which we

   719   will explain in this section.

   723   will explain in this section.