# HG changeset patch
# User wenzelm
# Date 876154942 -7200
# Node ID 38f8ec304b956243b63194192bc51a794845a703
# Parent  a99fdf465dfb10096d640ddae8100f9b4a7ef8b1
added sort_to_ast;
eliminated raise_ast;

diff -r a99fdf465dfb -r 38f8ec304b95 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Oct 06 18:21:00 1997 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Oct 06 18:22:22 1997 +0200
@@ -19,6 +19,7 @@
   include PRINTER0
   val term_to_ast: (string -> (typ -> term list -> term) option) -> term -> Ast.ast
   val typ_to_ast: (string -> (typ -> term list -> term) option) -> typ -> Ast.ast
+  val sort_to_ast: (string -> (typ -> term list -> term) option) -> sort -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
@@ -71,7 +72,7 @@
 
 
 
-(** typ_to_ast **)
+(** sort_to_ast, typ_to_ast **)
 
 fun ast_of_termT trf tm =
   let
@@ -83,7 +84,7 @@
           (case strip_comb t of
             (Const (a, _), args) => trans a args
           | (f, args) => Appl (map ast_of (f :: args)))
-      | ast_of t = raise_term "ast_of_termT: bad term encoding of type" [t]
+      | ast_of t = raise TERM ("ast_of_termT: bad term encoding of type", [t])
     and trans a args =
       (case trf a of
         Some f => ast_of (apply_trans "print translation" a (uncurry f) (dummyT, args))
@@ -93,6 +94,7 @@
     ast_of tm
   end;
 
+fun sort_to_ast trf S = ast_of_termT trf (term_of_sort S);
 fun typ_to_ast trf T = ast_of_termT trf (term_of_typ (! show_sorts) T);
 
 
@@ -346,7 +348,7 @@
       | astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
           combT (c, a, args, p)
       | astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
-      | astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
+      | astT (ast as Appl _, _) = raise AST ("pretty: malformed ast", [ast]);
   in
     astT (ast0, p0)
   end;