src/Pure/Syntax/parse_tree.ML

Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
of the error message ("The exception above was raised for...") will appear.
And print_exn calls print_sign_exn_unit so that it can re-raise the SAME
exception.

(*  Title:      Pure/Syntax/parse_tree.ML
    ID:         $Id$
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

TODO:
  move parsetree to parser.ML
  move pt_to_ast before ast_to_term (sextension.ML (?))
  delete this file
*)

signature PARSE_TREE =
sig
  structure Ast: AST
  structure Lexicon: LEXICON
  local open Ast Lexicon in
    datatype parsetree =
      Node of string * parsetree list |
      Tip of token
    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
  end
end;

functor ParseTreeFun(structure Ast: AST and Lexicon: LEXICON): PARSE_TREE =
struct

structure Ast = Ast;
structure Lexicon = Lexicon;
open Ast Lexicon;


(* datatype parsetree *)

datatype parsetree =
  Node of string * parsetree list |
  Tip of token;


(* pt_to_ast *)

fun pt_to_ast trf pt =
  let
    fun trans a args =
      (case trf a of
        None => mk_appl (Constant a) args
      | Some f => f args handle exn
          => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));

    fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
      | ast_of (Tip tok) = Variable (str_of_token tok);
  in
    ast_of pt
  end;


end;