diff -r 58bf09036a6d -r edb368e2878f src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Jun 29 15:13:40 2005 +0200 +++ b/src/Pure/Syntax/printer.ML Wed Jun 29 15:13:41 2005 +0200 @@ -18,19 +18,22 @@ signature PRINTER = sig include PRINTER0 - val term_to_ast: (string -> (bool -> typ -> term list -> term) list) -> term -> Ast.ast - val typ_to_ast: (string -> (bool -> typ -> term list -> term) list) -> typ -> Ast.ast - val sort_to_ast: (string -> (bool -> typ -> term list -> term) list) -> sort -> Ast.ast + val term_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) -> + term -> Ast.ast + val typ_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) -> + typ -> Ast.ast + val sort_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) -> + sort -> Ast.ast type prtabs val empty_prtabs: prtabs val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs val merge_prtabs: prtabs -> prtabs -> prtabs - val pretty_term_ast: bool -> prtabs - -> (string -> (Ast.ast list -> Ast.ast) list) + val pretty_term_ast: theory -> bool -> prtabs + -> (string -> (theory -> Ast.ast list -> Ast.ast) list) -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T - val pretty_typ_ast: bool -> prtabs - -> (string -> (Ast.ast list -> Ast.ast) list) + val pretty_typ_ast: theory -> bool -> prtabs + -> (string -> (theory -> Ast.ast list -> Ast.ast) list) -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T end; @@ -55,15 +58,17 @@ (* apply print (ast) translation function *) -fun apply_first [] x = raise Match - | apply_first (f :: fs) x = f x handle Match => apply_first fs x; +fun apply_trans thy name a fns args = + let + fun app_first [] = raise Match + | app_first (f :: fs) = f thy args handle Match => app_first fs; + in + transform_failure (fn Match => Match + | exn => SynTrans.TRANSLATION_FAIL (exn, "Error in " ^ name ^ " for " ^ quote a)) + app_first fns + end; -fun apply_trans name a fs args = - (apply_first fs args handle - Match => raise Match - | exn => (priority ("Error in " ^ name ^ " for " ^ quote a); raise exn)); - -fun apply_typed x y fs = map (fn f => f x y) fs; +fun apply_typed x y fs = map (fn f => fn thy => f thy x y) fs; (* simple_ast_of *) @@ -82,7 +87,7 @@ (** sort_to_ast, typ_to_ast **) -fun ast_of_termT trf tm = +fun ast_of_termT thy trf tm = let fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t @@ -94,12 +99,12 @@ | (f, args) => Ast.Appl (map ast_of (f :: args))) | ast_of t = simple_ast_of t and trans a args = - ast_of (apply_trans "print translation" a (apply_typed false dummyT (trf a)) args) + ast_of (apply_trans thy "print translation" a (apply_typed false dummyT (trf a)) args) handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); in ast_of tm end; -fun sort_to_ast trf S = ast_of_termT trf (TypeExt.term_of_sort S); -fun typ_to_ast trf T = ast_of_termT trf (TypeExt.term_of_typ (! show_sorts) T); +fun sort_to_ast thy trf S = ast_of_termT thy trf (TypeExt.term_of_sort S); +fun typ_to_ast thy trf T = ast_of_termT thy trf (TypeExt.term_of_typ (! show_sorts) T); @@ -116,7 +121,7 @@ else Lexicon.const "_var" $ t | mark_freevars a = a; -fun ast_of_term trf show_all_types no_freeTs show_types show_sorts tm = +fun ast_of_term thy trf show_all_types no_freeTs show_types show_sorts tm = let fun prune_typs (t_seen as (Const _, _)) = t_seen | prune_typs (t as Free (x, ty), seen) = @@ -153,13 +158,13 @@ | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts)) and trans a T args = - ast_of (apply_trans "print translation" a (apply_typed show_sorts T (trf a)) args) + ast_of (apply_trans thy "print translation" a (apply_typed show_sorts T (trf a)) args) handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) and constrain t T = if show_types andalso T <> dummyT then Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t, - ast_of_termT trf (TypeExt.term_of_typ show_sorts T)] + ast_of_termT thy trf (TypeExt.term_of_typ show_sorts T)] else simple_ast_of t in tm @@ -169,8 +174,8 @@ |> ast_of end; -fun term_to_ast trf tm = - ast_of_term trf (! show_all_types) (! show_no_free_types) +fun term_to_ast thy trf tm = + ast_of_term thy trf (! show_all_types) (! show_no_free_types) (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm; @@ -260,9 +265,9 @@ | is_chain [Arg _] = true | is_chain _ = false; -fun pretty tabs trf tokentrf type_mode curried ast0 p0 = +fun pretty thy tabs trf tokentrf type_mode curried ast0 p0 = let - val trans = apply_trans "print ast translation"; + val trans = apply_trans thy "print ast translation"; fun token_trans c [Ast.Variable x] = (case tokentrf c of @@ -285,7 +290,7 @@ val (Ts, args') = synT (symbs, args); in if type_mode then (astT (t, p) @ Ts, args') - else (pretty tabs trf tokentrf true curried t p @ Ts, args') + else (pretty thy tabs trf tokentrf true curried t p @ Ts, args') end | synT (String s :: symbs, args) = let val (Ts, args') = synT (symbs, args); @@ -312,10 +317,7 @@ else pr, args)) and prefixT (_, a, [], _) = [Pretty.str a] - | prefixT (c, _, args, p) = - if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then - [Pretty.str "*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***"] - else astT (appT (c, args), p) + | prefixT (c, _, args, p) = astT (appT (c, args), p) and splitT 0 ([x], ys) = (x, ys) | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) @@ -351,15 +353,15 @@ (* pretty_term_ast *) -fun pretty_term_ast curried prtabs trf tokentrf ast = - Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode)) +fun pretty_term_ast thy curried prtabs trf tokentrf ast = + Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode)) trf tokentrf false curried ast 0); (* pretty_typ_ast *) -fun pretty_typ_ast _ prtabs trf tokentrf ast = - Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode)) +fun pretty_typ_ast thy _ prtabs trf tokentrf ast = + Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode)) trf tokentrf true false ast 0); end;