--- 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;