equal
deleted
inserted
replaced
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 -> |