src/Doc/IsarRef/Outer_Syntax.thy
changeset 51062 d5fd24f73555
parent 51058 98c48d023136
child 53015 a1119cf551e8
equal deleted inserted replaced
51061:1f184f8ec10b 51062:d5fd24f73555
    41   clearly recognized from the input syntax, e.g.\ encounter of the
    41   clearly recognized from the input syntax, e.g.\ encounter of the
    42   next command keyword.
    42   next command keyword.
    43 
    43 
    44   More advanced interfaces such as Isabelle/jEdit \cite{Wenzel:2012}
    44   More advanced interfaces such as Isabelle/jEdit \cite{Wenzel:2012}
    45   and Proof~General \cite{proofgeneral} do not require explicit
    45   and Proof~General \cite{proofgeneral} do not require explicit
    46   semicolons, the amount of input text is determined automatically by
    46   semicolons: command spans are determined by inspecting the content
    47   inspecting the present content of the Emacs text buffer.  In the
    47   of the editor buffer.  In the printed presentation of Isabelle/Isar
    48   printed presentation of Isabelle/Isar documents semicolons are
    48   documents semicolons are omitted altogether for readability.
    49   omitted altogether for readability.
       
    50 
    49 
    51   \begin{warn}
    50   \begin{warn}
    52     Proof~General requires certain syntax classification tables in
    51     Proof~General requires certain syntax classification tables in
    53     order to achieve properly synchronized interaction with the
    52     order to achieve properly synchronized interaction with the
    54     Isabelle/Isar process.  These tables need to be consistent with
    53     Isabelle/Isar process.  These tables need to be consistent with