src/Pure/Isar/isar_cmd.ML
changeset 52143 36ffe23b25f8
parent 51717 9e7d1c139569
child 52549 802576856527
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  sig
     1.5    val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
     1.6    val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
     1.7 -  val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.8 -  val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.9 -  val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    1.10 -  val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    1.11 -  val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    1.12 +  val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.13 +  val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.14 +  val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.15 +  val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.16 +  val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.17    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    1.18    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    1.19    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    1.20 @@ -85,57 +85,41 @@
    1.21  
    1.22  (* translation functions *)
    1.23  
    1.24 -local
    1.25 -
    1.26 -fun advancedT false = ""
    1.27 -  | advancedT true = "Proof.context -> ";
    1.28 -
    1.29 -fun advancedN false = ""
    1.30 -  | advancedN true = "advanced_";
    1.31 -
    1.32 -in
    1.33 -
    1.34 -fun parse_ast_translation (a, (txt, pos)) =
    1.35 +fun parse_ast_translation (txt, pos) =
    1.36    ML_Lex.read pos txt
    1.37    |> ML_Context.expression pos
    1.38 -    ("val parse_ast_translation: (string * (" ^ advancedT a ^
    1.39 -      "Ast.ast list -> Ast.ast)) list")
    1.40 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
    1.41 +    "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.42 +    "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.43    |> Context.theory_map;
    1.44  
    1.45 -fun parse_translation (a, (txt, pos)) =
    1.46 +fun parse_translation (txt, pos) =
    1.47 +  ML_Lex.read pos txt
    1.48 +  |> ML_Context.expression pos
    1.49 +    "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    1.50 +    "Context.map_theory (Sign.parse_translation parse_translation)"
    1.51 +  |> Context.theory_map;
    1.52 +
    1.53 +fun print_translation (txt, pos) =
    1.54    ML_Lex.read pos txt
    1.55    |> ML_Context.expression pos
    1.56 -    ("val parse_translation: (string * (" ^ advancedT a ^
    1.57 -      "term list -> term)) list")
    1.58 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    1.59 -  |> Context.theory_map;
    1.60 -
    1.61 -fun print_translation (a, (txt, pos)) =
    1.62 -  ML_Lex.read pos txt
    1.63 -  |> ML_Context.expression pos
    1.64 -    ("val print_translation: (string * (" ^ advancedT a ^
    1.65 -      "term list -> term)) list")
    1.66 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    1.67 +    "val print_translation: (string * (Proof.context -> term list -> term)) list"
    1.68 +    "Context.map_theory (Sign.print_translation print_translation)"
    1.69    |> Context.theory_map;
    1.70  
    1.71 -fun print_ast_translation (a, (txt, pos)) =
    1.72 +fun typed_print_translation (txt, pos) =
    1.73    ML_Lex.read pos txt
    1.74    |> ML_Context.expression pos
    1.75 -    ("val print_ast_translation: (string * (" ^ advancedT a ^
    1.76 -      "Ast.ast list -> Ast.ast)) list")
    1.77 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    1.78 +    "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    1.79 +    "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    1.80    |> Context.theory_map;
    1.81  
    1.82 -fun typed_print_translation (a, (txt, pos)) =
    1.83 +fun print_ast_translation (txt, pos) =
    1.84    ML_Lex.read pos txt
    1.85    |> ML_Context.expression pos
    1.86 -    ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
    1.87 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    1.88 +    "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.89 +    "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.90    |> Context.theory_map;
    1.91  
    1.92 -end;
    1.93 -
    1.94  
    1.95  (* translation rules *)
    1.96