src/Pure/Thy/thy_output.ML
changeset 49321 a48f9bbbe720
parent 49244 fb669aff821e
child 49847 ed5080c03165
equal deleted inserted replaced
49320:94bd2fb83d11 49321:a48f9bbbe720
    81 (
    81 (
    82   type T =
    82   type T =
    83     (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    83     (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    84       (string -> Proof.context -> Proof.context) Name_Space.table;
    84       (string -> Proof.context -> Proof.context) Name_Space.table;
    85   val empty : T =
    85   val empty : T =
    86     (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
    86     (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
    87       Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
    87       Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
    88   val extend = I;
    88   val extend = I;
    89   fun merge ((commands1, options1), (commands2, options2)) : T =
    89   fun merge ((commands1, options1), (commands2, options2)) : T =
    90     (Name_Space.merge_tables (commands1, commands2),
    90     (Name_Space.merge_tables (commands1, commands2),
    91       Name_Space.merge_tables (options1, options2));
    91       Name_Space.merge_tables (options1, options2));
    92 );
    92 );