src/Pure/Isar/outer_syntax.ML
changeset 30513 1796b8ea88aa
parent 29428 3ab54b42ded8
child 30573 49899f26fbd1
equal deleted inserted replaced
30512:17b2aad869fa 30513:1796b8ea88aa
     7 beginning; for interactive processing it may change dynamically.
     7 beginning; for interactive processing it may change dynamically.
     8 *)
     8 *)
     9 
     9 
    10 signature OUTER_SYNTAX =
    10 signature OUTER_SYNTAX =
    11 sig
    11 sig
    12   type 'a parser = 'a OuterParse.parser
       
    13   val command: string -> string -> OuterKeyword.T ->
    12   val command: string -> string -> OuterKeyword.T ->
    14     (Toplevel.transition -> Toplevel.transition) parser -> unit
    13     (Toplevel.transition -> Toplevel.transition) parser -> unit
    15   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
    14   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
    16     (Toplevel.transition -> Toplevel.transition) parser -> unit
    15     (Toplevel.transition -> Toplevel.transition) parser -> unit
    17   val improper_command: string -> string -> OuterKeyword.T ->
    16   val improper_command: string -> string -> OuterKeyword.T ->