moved ML translation interfaces to isar_cmd.ML;
authorwenzelm
Fri Jan 19 22:08:20 2007 +0100 (2007-01-19)
changeset 22111b3f5b654bcd3
parent 22110 f9eb6328bdbd
child 22112 6a90ac654c6d
moved ML translation interfaces to isar_cmd.ML;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Jan 19 22:08:19 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Jan 19 22:08:20 2007 +0100
     1.3 @@ -46,12 +46,6 @@
     1.4      (string * string * (string -> string * real)) list -> theory -> theory
     1.5    val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
     1.6      -> theory -> theory
     1.7 -  val parse_ast_translation: bool * string -> theory -> theory
     1.8 -  val parse_translation: bool * string -> theory -> theory
     1.9 -  val print_translation: bool * string -> theory -> theory
    1.10 -  val typed_print_translation: bool * string -> theory -> theory
    1.11 -  val print_ast_translation: bool * string -> theory -> theory
    1.12 -  val token_translation: string -> theory -> theory
    1.13    val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    1.14    val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    1.15    val add_trrules_i: ast Syntax.trrule list -> theory -> theory
    1.16 @@ -825,56 +819,6 @@
    1.17  fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
    1.18  
    1.19  
    1.20 -(* compile translation functions *)
    1.21 -
    1.22 -local
    1.23 -
    1.24 -fun advancedT false = ""
    1.25 -  | advancedT true = "Proof.context -> ";
    1.26 -
    1.27 -fun advancedN false = ""
    1.28 -  | advancedN true = "advanced_";
    1.29 -
    1.30 -in
    1.31 -
    1.32 -fun parse_ast_translation (a, txt) =
    1.33 -  txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
    1.34 -      "Syntax.ast list -> Syntax.ast)) list")
    1.35 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
    1.36 -  |> Context.theory_map;
    1.37 -
    1.38 -fun parse_translation (a, txt) =
    1.39 -  txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
    1.40 -      "term list -> term)) list")
    1.41 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    1.42 -  |> Context.theory_map;
    1.43 -
    1.44 -fun print_translation (a, txt) =
    1.45 -  txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
    1.46 -      "term list -> term)) list")
    1.47 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    1.48 -  |> Context.theory_map;
    1.49 -
    1.50 -fun print_ast_translation (a, txt) =
    1.51 -  txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
    1.52 -      "Syntax.ast list -> Syntax.ast)) list")
    1.53 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    1.54 -  |> Context.theory_map;
    1.55 -
    1.56 -fun typed_print_translation (a, txt) =
    1.57 -  txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
    1.58 -      "bool -> typ -> term list -> term)) list")
    1.59 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    1.60 -  |> Context.theory_map;
    1.61 -
    1.62 -val token_translation =
    1.63 -  Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
    1.64 -    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
    1.65 -  #> Context.theory_map;
    1.66 -
    1.67 -end;
    1.68 -
    1.69 -
    1.70  (* translation rules *)
    1.71  
    1.72  fun gen_trrules f args thy = thy |> map_syn (fn syn =>