src/Pure/Syntax/syn_trans.ML
changeset 42204 b3277168c1e7
parent 42153 fa108629d132
child 42223 098c86e53153
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4      (string * (term list -> term)) list *
     1.5      (string * (bool -> typ -> term list -> term)) list *
     1.6      (string * (Ast.ast list -> Ast.ast)) list
     1.7 +  type type_context
     1.8  end;
     1.9  
    1.10  signature SYN_TRANS =
    1.11 @@ -57,8 +58,9 @@
    1.12    val prop_tr': term -> term
    1.13    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.14    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.15 -  val parsetree_to_ast: Proof.context -> bool ->
    1.16 -    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    1.17 +  val parsetree_to_ast: Proof.context -> type_context -> bool ->
    1.18 +    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
    1.19 +    Parser.parsetree -> Position.reports * Ast.ast
    1.20    val ast_to_term: Proof.context ->
    1.21      (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
    1.22  end;
    1.23 @@ -549,21 +551,44 @@
    1.24  
    1.25  (** parsetree_to_ast **)
    1.26  
    1.27 -fun parsetree_to_ast ctxt constrain_pos trf =
    1.28 +type type_context =
    1.29 + {get_class: string -> string,
    1.30 +  get_type: string -> string,
    1.31 +  markup_class: string -> Markup.T list,
    1.32 +  markup_type: string -> Markup.T list};
    1.33 +
    1.34 +fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
    1.35    let
    1.36 +    val {get_class, get_type, markup_class, markup_type} = type_context;
    1.37 +
    1.38 +    val reports = Unsynchronized.ref ([]: Position.reports);
    1.39 +    fun report pos = Position.reports reports [pos];
    1.40 +
    1.41      fun trans a args =
    1.42        (case trf a of
    1.43          NONE => Ast.mk_appl (Ast.Constant a) args
    1.44        | SOME f => f ctxt args);
    1.45  
    1.46 -    fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
    1.47 +    fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    1.48 +          let
    1.49 +            val c = get_class (Lexicon.str_of_token tok);
    1.50 +            val _ = report (Lexicon.pos_of_token tok) markup_class c;
    1.51 +          in Ast.Constant (Lexicon.mark_class c) end
    1.52 +      | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
    1.53 +          let
    1.54 +            val c = get_type (Lexicon.str_of_token tok);
    1.55 +            val _ = report (Lexicon.pos_of_token tok) markup_type c;
    1.56 +          in Ast.Constant (Lexicon.mark_type c) end
    1.57 +      | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
    1.58            if constrain_pos then
    1.59              Ast.Appl [Ast.Constant "_constrain", ast_of pt,
    1.60                Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
    1.61            else ast_of pt
    1.62        | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    1.63        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    1.64 -  in ast_of end;
    1.65 +
    1.66 +    val ast = ast_of parsetree;
    1.67 +  in (! reports, ast) end;
    1.68  
    1.69  
    1.70