# HG changeset patch # User wenzelm # Date 1302102040 -7200 # Node ID f427c9890c46596e08d72f3349689187ba63bb03 # Parent c539d3c9c023a67cf5f772d8a57ef9b584ee748e more abstract print translation; diff -r c539d3c9c023 -r f427c9890c46 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Apr 06 16:15:57 2011 +0200 +++ b/src/Pure/Syntax/printer.ML Wed Apr 06 17:00:40 2011 +0200 @@ -23,7 +23,6 @@ val show_question_marks_raw: Config.raw val show_question_marks: bool Config.T val pretty_priority: int Config.T - val apply_trans: 'a -> ('a -> 'b -> 'c) list -> 'b -> 'c end; signature PRINTER = @@ -36,11 +35,11 @@ val merge_prtabs: prtabs -> prtabs -> prtabs val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring, extern_const: string -> xstring} -> Proof.context -> bool -> prtabs -> - (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) -> + (string -> Proof.context -> Ast.ast list -> Ast.ast) -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} -> Proof.context -> bool -> prtabs -> - (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) -> + (string -> Proof.context -> Ast.ast list -> Ast.ast) -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list end; @@ -161,12 +160,6 @@ (** pretty term or typ asts **) -fun apply_trans ctxt fns args = - let - fun app_first [] = raise Match - | app_first (f :: fs) = f ctxt args handle Match => app_first fs; - in app_first fns end; - fun is_chain [Block (_, pr)] = is_chain pr | is_chain [Arg _] = true | is_chain _ = false; @@ -264,7 +257,7 @@ in (case tokentrT a args of SOME prt => [prt] - | NONE => astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs)) + | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs)) end and tokentrT a [Ast.Variable x] = token_trans a x diff -r c539d3c9c023 -r f427c9890c46 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Apr 06 16:15:57 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Apr 06 17:00:40 2011 +0200 @@ -120,8 +120,10 @@ val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option - val print_translation: syntax -> string -> (Proof.context -> typ -> term list -> term) list - val print_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) list + val print_translation: syntax -> string -> + Proof.context -> typ -> term list -> term (*exception Match*) + val print_ast_translation: syntax -> string -> + Proof.context -> Ast.ast list -> Ast.ast (*exception Match*) val token_translation: syntax -> string list -> string -> (Proof.context -> string -> Pretty.T) option type mode @@ -421,7 +423,19 @@ (* print (ast) translations *) -fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c); +fun apply_tr' tab c ctxt T args = + let + val fns = map fst (Symtab.lookup_list tab c); + fun app_first [] = raise Match + | app_first (f :: fs) = f ctxt T args handle Match => app_first fs; + in app_first fns end; + +fun apply_ast_tr' tab c ctxt args = + let + val fns = map fst (Symtab.lookup_list tab c); + fun app_first [] = raise Match + | app_first (f :: fs) = f ctxt args handle Match => app_first fs; + in app_first fns end; fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns; fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns; @@ -507,8 +521,8 @@ fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; -fun print_translation (Syntax ({print_trtab, ...}, _)) = lookup_tr' print_trtab; -fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = lookup_tr' print_ast_trtab; +fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab; +fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab; fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab; type mode = string * bool; diff -r c539d3c9c023 -r f427c9890c46 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 16:15:57 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 17:00:40 2011 +0200 @@ -443,8 +443,6 @@ (* sort_to_ast and typ_to_ast *) -fun apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs; - fun ast_of_termT ctxt trf tm = let val ctxt' = Config.put show_sorts false ctxt; @@ -456,9 +454,8 @@ (Const (a, _), args) => trans a args | (f, args) => Ast.Appl (map ast_of (f :: args))) | ast_of t = simple_ast_of ctxt t - and trans a args = - ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args) - handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); + and trans a args = ast_of (trf a ctxt' dummyT args) + handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); in ast_of tm end; fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S); @@ -535,9 +532,8 @@ else trans c T ts | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) - and trans a T args = - ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args) - handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) + and trans a T args = ast_of (trf a ctxt T args) + handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) and constrain t T = if show_types andalso T <> dummyT then @@ -564,7 +560,7 @@ val tr' = Syntax.print_translation syn; val ast_tr' = Syntax.print_ast_translation syn; val tokentr = Syntax.token_translation syn (print_mode_value ()); - val {print_ruletab, tokentrtab, prtabs, ...} = Syntax.rep_syntax syn; + val {print_ruletab, prtabs, ...} = Syntax.rep_syntax syn; in t_to_ast ctxt tr' t |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab)