token translations: context dependent, result Pretty.T;
authorwenzelm
Thu Apr 17 16:30:50 2008 +0200 (2008-04-17)
changeset 2670451ee753cc2e3
parent 26703 c07b1a90600c
child 26705 334d3fa649ea
token translations: context dependent, result Pretty.T;
string_of_term/prop: Variable.auto_fixes;
src/Pure/Isar/isar_cmd.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 17 16:30:48 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 17 16:30:50 2008 +0200
     1.3 @@ -186,7 +186,7 @@
     1.4  
     1.5  fun token_translation (txt, pos) =
     1.6    txt |> ML_Context.expression pos
     1.7 -    "val token_translation: (string * string * (string -> output * int)) list"
     1.8 +    "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list"
     1.9        "Context.map_theory (Sign.add_tokentrfuns token_translation)"
    1.10    |> Context.theory_map;
    1.11  
    1.12 @@ -602,17 +602,19 @@
    1.13    let
    1.14      val ctxt = Proof.context_of state;
    1.15      val prop = Syntax.read_prop ctxt s;
    1.16 -  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
    1.17 +    val ctxt' = Variable.auto_fixes prop ctxt;
    1.18 +  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
    1.19  
    1.20  fun string_of_term state s =
    1.21    let
    1.22      val ctxt = Proof.context_of state;
    1.23      val t = Syntax.read_term ctxt s;
    1.24      val T = Term.type_of t;
    1.25 +    val ctxt' = Variable.auto_fixes t ctxt;
    1.26    in
    1.27      Pretty.string_of
    1.28 -      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
    1.29 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
    1.30 +      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
    1.31 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
    1.32    end;
    1.33  
    1.34  fun string_of_type state s =
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Apr 17 16:30:48 2008 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Apr 17 16:30:50 2008 +0200
     2.3 @@ -14,8 +14,9 @@
     2.4    val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
     2.5    val mk_trfun: string * 'a -> string * ('a * stamp)
     2.6    val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
     2.7 -  val tokentrans_mode: string -> (string * (string -> output * int)) list ->
     2.8 -    (string * string * (string -> output * int)) list
     2.9 +  val tokentrans_mode:
    2.10 +    string -> (string * (Proof.context -> string -> Pretty.T)) list ->
    2.11 +    (string * string * (Proof.context -> string -> Pretty.T)) list
    2.12    val standard_token_classes: string list
    2.13  end;
    2.14  
    2.15 @@ -49,7 +50,7 @@
    2.16          (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    2.17        print_rules: (Ast.ast * Ast.ast) list,
    2.18        print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    2.19 -      token_translation: (string * string * (string -> output * int)) list}
    2.20 +      token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
    2.21    val mfix_delims: string -> string list
    2.22    val mfix_args: string -> int
    2.23    val escape_mfix: string -> string
    2.24 @@ -58,14 +59,14 @@
    2.25      (string * ((Proof.context -> term list -> term) * stamp)) list *
    2.26      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    2.27      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    2.28 -    -> (string * string * (string -> output * int)) list
    2.29 +    -> (string * string * (Proof.context -> string -> Pretty.T)) list
    2.30      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.31    val syn_ext: mfix list -> string list ->
    2.32      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    2.33      (string * ((Proof.context -> term list -> term) * stamp)) list *
    2.34      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    2.35      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    2.36 -    -> (string * string * (string -> output * int)) list
    2.37 +    -> (string * string * (Proof.context -> string -> Pretty.T)) list
    2.38      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.39    val syn_ext_const_names: string list -> syn_ext
    2.40    val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.41 @@ -79,7 +80,7 @@
    2.42      (string * ((Proof.context -> term list -> term) * stamp)) list *
    2.43      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    2.44      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    2.45 -  val syn_ext_tokentrfuns: (string * string * (string -> output * int)) list -> syn_ext
    2.46 +  val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
    2.47    val standard_token_markers: string list
    2.48    val pure_ext: syn_ext
    2.49  end;
    2.50 @@ -334,7 +335,7 @@
    2.51        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    2.52      print_rules: (Ast.ast * Ast.ast) list,
    2.53      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    2.54 -    token_translation: (string * string * (string -> output * int)) list};
    2.55 +    token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};
    2.56  
    2.57  
    2.58  (* syn_ext *)
     3.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:48 2008 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:50 2008 +0200
     3.3 @@ -45,7 +45,8 @@
     3.4      (string * ((Proof.context -> term list -> term) * stamp)) list *
     3.5      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     3.6      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
     3.7 -  val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
     3.8 +  val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
     3.9 +    syntax -> syntax
    3.10    val update_const_gram: (string -> bool) ->
    3.11      mode -> (string * typ * mixfix) list -> syntax -> syntax
    3.12    val remove_const_gram: (string -> bool) ->
    3.13 @@ -239,7 +240,7 @@
    3.14      print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    3.15      print_ruletab: ruletab,
    3.16      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    3.17 -    tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
    3.18 +    tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
    3.19      prtabs: Printer.prtabs} * stamp;
    3.20  
    3.21  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;