src/Pure/sign.ML
changeset 17102 a83a80f1c8dd
parent 17039 78159411623f
child 17184 3d80209e9a53
     1.1 --- a/src/Pure/sign.ML	Thu Aug 18 11:17:36 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Aug 18 11:17:37 2005 +0200
     1.3 @@ -49,6 +49,12 @@
     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 add_trrules_i: ast Syntax.trrule list -> theory -> theory
    1.15    val add_path: string -> theory -> theory
    1.16 @@ -774,6 +780,50 @@
    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 = "theory -> ";
    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 +    ("Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], [])");
    1.36 +
    1.37 +fun parse_translation (a, txt) =
    1.38 +  txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
    1.39 +      "term list -> term)) list")
    1.40 +    ("Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], [])");
    1.41 +
    1.42 +fun print_translation (a, txt) =
    1.43 +  txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
    1.44 +      "term list -> term)) list")
    1.45 +    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, [])");
    1.46 +
    1.47 +fun print_ast_translation (a, txt) =
    1.48 +  txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
    1.49 +      "Syntax.ast list -> Syntax.ast)) list")
    1.50 +    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation)");
    1.51 +
    1.52 +fun typed_print_translation (a, txt) =
    1.53 +  txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
    1.54 +      "bool -> typ -> term list -> term)) list")
    1.55 +    ("Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation");
    1.56 +
    1.57 +val token_translation =
    1.58 +  Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
    1.59 +    "Sign.add_tokentrfuns token_translation";
    1.60 +
    1.61 +end;
    1.62 +
    1.63 +
    1.64  (* add translation rules *)
    1.65  
    1.66  fun add_trrules args thy = thy |> map_syn (fn syn =>