proper position for decode_pos, which is relevant for completion;
authorwenzelm
Thu Mar 06 19:55:08 2014 +0100 (2014-03-06)
changeset 55960beef468837b1
parent 55959 c3b458435f4f
child 55961 c2d4a3608441
proper position for decode_pos, which is relevant for completion;
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 17:37:32 2014 +0100
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 19:55:08 2014 +0100
     1.3 @@ -811,16 +811,15 @@
     1.4  
     1.5  (* authentic syntax *)
     1.6  
     1.7 -fun const_ast_tr intern ctxt [Ast.Variable c] =
     1.8 +fun const_ast_tr intern ctxt asts =
     1.9 +  (case asts of
    1.10 +    [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
    1.11        let
    1.12 -        val (c', _) = decode_const ctxt (c, []);
    1.13 +        val pos = the_default Position.none (Term_Position.decode p);
    1.14 +        val (c', _) = decode_const ctxt (c, [pos]);
    1.15          val d = if intern then Lexicon.mark_const c' else c;
    1.16 -      in Ast.Constant d end
    1.17 -  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
    1.18 -      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
    1.19 -        handle ERROR msg =>
    1.20 -          error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
    1.21 -  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
    1.22 +      in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
    1.23 +  | _ => raise Ast.AST ("const_ast_tr", asts));
    1.24  
    1.25  
    1.26  (* setup translations *)