src/Pure/Isar/outer_syntax.ML
changeset 29380 a9ee3475abf4
parent 29315 b074c05f00ad
child 29428 3ab54b42ded8
equal deleted inserted replaced
29379:f65670092259 29380:a9ee3475abf4
    15   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
    15   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
    16     (Toplevel.transition -> Toplevel.transition) parser -> unit
    16     (Toplevel.transition -> Toplevel.transition) parser -> unit
    17   val improper_command: string -> string -> OuterKeyword.T ->
    17   val improper_command: string -> string -> OuterKeyword.T ->
    18     (Toplevel.transition -> Toplevel.transition) parser -> unit
    18     (Toplevel.transition -> Toplevel.transition) parser -> unit
    19   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
    19   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
       
    20   val local_theory': string -> string -> OuterKeyword.T ->
       
    21     (bool -> local_theory -> local_theory) parser -> unit
    20   val local_theory: string -> string -> OuterKeyword.T ->
    22   val local_theory: string -> string -> OuterKeyword.T ->
    21     (local_theory -> local_theory) parser -> unit
    23     (local_theory -> local_theory) parser -> unit
    22   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
    24   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
    23     (bool -> local_theory -> Proof.state) parser -> unit
    25     (bool -> local_theory -> Proof.state) parser -> unit
    24   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
    26   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
   136 
   138 
   137 fun local_theory_command do_print trans name comment kind parse =
   139 fun local_theory_command do_print trans name comment kind parse =
   138   command name comment kind (P.opt_target -- parse
   140   command name comment kind (P.opt_target -- parse
   139     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   141     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   140 
   142 
       
   143 val local_theory' = local_theory_command false Toplevel.local_theory';
   141 val local_theory = local_theory_command false Toplevel.local_theory;
   144 val local_theory = local_theory_command false Toplevel.local_theory;
   142 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   145 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   143 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   146 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   144 
   147 
   145 
   148