src/Pure/Isar/isar_cmd.ML
changeset 42204 b3277168c1e7
parent 41435 12585dfb86fe
child 42224 578a51fae383
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.5    val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.6    val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.7 +  val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.8 +  val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.9    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    1.10    val add_axioms: (Attrib.binding * string) list -> theory -> theory
    1.11    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    1.12 @@ -154,6 +156,22 @@
    1.13  end;
    1.14  
    1.15  
    1.16 +(* translation rules *)
    1.17 +
    1.18 +fun read_trrules thy raw_rules =
    1.19 +  let
    1.20 +    val ctxt = ProofContext.init_global thy;
    1.21 +    val type_ctxt = ProofContext.type_context ctxt;
    1.22 +    val syn = ProofContext.syn_of ctxt;
    1.23 +  in
    1.24 +    raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
    1.25 +      Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
    1.26 +  end;
    1.27 +
    1.28 +fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
    1.29 +fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
    1.30 +
    1.31 +
    1.32  (* oracles *)
    1.33  
    1.34  fun oracle (name, pos) (body_txt, body_pos) =