removed exotic 'token_translation' command;
authorwenzelm
Sat Jun 14 17:26:07 2008 +0200 (2008-06-14 ago)
changeset 2720000b7b55b61bd
parent 27199 0a451e1e6176
child 27201 e0323036bcf2
removed exotic 'token_translation' command;
NEWS
doc-src/IsarRef/Thy/Spec.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Sat Jun 14 15:58:36 2008 +0200
     1.2 +++ b/NEWS	Sat Jun 14 17:26:07 2008 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4  
     1.5  * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
     1.6  
     1.7 +* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
     1.8 +interface instead.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Jun 14 15:58:36 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Jun 14 17:26:07 2008 +0200
     2.3 @@ -1262,16 +1262,12 @@
     2.4      @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
     2.5      @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
     2.6      @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
     2.7 -    @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
     2.8    \end{matharray}
     2.9  
    2.10    \begin{rail}
    2.11    ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
    2.12      'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
    2.13    ;
    2.14 -
    2.15 -  'token\_translation' text
    2.16 -  ;
    2.17    \end{rail}
    2.18  
    2.19    Syntax translation functions written in ML admit almost arbitrary
    2.20 @@ -1287,8 +1283,6 @@
    2.21  val typed_print_translation :
    2.22    (string * (bool -> typ -> term list -> term)) list
    2.23  val print_ast_translation   : (string * (ast list -> ast)) list
    2.24 -val token_translation       :
    2.25 -  (string * string * (string -> string * real)) list
    2.26  \end{ttbox}
    2.27  
    2.28    If the @{text "(advanced)"} option is given, the corresponding
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Jun 14 15:58:36 2008 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Jun 14 17:26:07 2008 +0200
     3.3 @@ -13,7 +13,6 @@
     3.4    val print_translation: bool * (string * Position.T) -> theory -> theory
     3.5    val typed_print_translation: bool * (string * Position.T) -> theory -> theory
     3.6    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
     3.7 -  val token_translation: string * Position.T -> theory -> theory
     3.8    val oracle: bstring -> string -> string * Position.T -> theory -> theory
     3.9    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    3.10    val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    3.11 @@ -184,12 +183,6 @@
    3.12      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    3.13    |> Context.theory_map;
    3.14  
    3.15 -fun token_translation (txt, pos) =
    3.16 -  txt |> ML_Context.expression pos
    3.17 -    "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list"
    3.18 -      "Context.map_theory (Sign.add_tokentrfuns token_translation)"
    3.19 -  |> Context.theory_map;
    3.20 -
    3.21  end;
    3.22  
    3.23  
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jun 14 15:58:36 2008 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 14 17:26:07 2008 +0200
     4.3 @@ -361,11 +361,6 @@
     4.4      (K.tag_ml K.thy_decl)
     4.5      (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
     4.6  
     4.7 -val _ =
     4.8 -  OuterSyntax.command "token_translation" "install token translation functions"
     4.9 -    (K.tag_ml K.thy_decl)
    4.10 -    (P.position P.text >> (Toplevel.theory o IsarCmd.token_translation));
    4.11 -
    4.12  
    4.13  (* oracles *)
    4.14