more precise error positions;
authorwenzelm
Sat Apr 23 19:22:11 2011 +0200 (2011-04-23)
changeset 42470cc78b0ed0fad
parent 42469 daa93275880e
child 42471 593289343c7d
more precise error positions;
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Apr 23 18:46:01 2011 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Apr 23 19:22:11 2011 +0200
     1.3 @@ -125,9 +125,6 @@
     1.4  
     1.5  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
     1.6    let
     1.7 -    val get_class = Proof_Context.read_class ctxt;
     1.8 -    val get_type = #1 o dest_Type o Proof_Context.read_type_name_proper ctxt false;
     1.9 -
    1.10      val reports = Unsynchronized.ref ([]: Position.reports);
    1.11      fun report pos = Position.reports reports [pos];
    1.12  
    1.13 @@ -138,13 +135,18 @@
    1.14  
    1.15      fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    1.16            let
    1.17 -            val c = get_class (Lexicon.str_of_token tok);
    1.18 -            val _ = report (Lexicon.pos_of_token tok) (markup_class ctxt) c;
    1.19 +            val pos = Lexicon.pos_of_token tok;
    1.20 +            val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
    1.21 +              handle ERROR msg => error (msg ^ Position.str_of pos);
    1.22 +            val _ = report pos (markup_class ctxt) c;
    1.23            in [Ast.Constant (Lexicon.mark_class c)] end
    1.24        | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
    1.25            let
    1.26 -            val c = get_type (Lexicon.str_of_token tok);
    1.27 -            val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
    1.28 +            val pos = Lexicon.pos_of_token tok;
    1.29 +            val Type (c, _) =
    1.30 +              Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
    1.31 +                handle ERROR msg => error (msg ^ Position.str_of pos);
    1.32 +            val _ = report pos (markup_type ctxt) c;
    1.33            in [Ast.Constant (Lexicon.mark_type c)] end
    1.34        | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
    1.35            if constrain_pos then
    1.36 @@ -352,11 +354,11 @@
    1.37        val level = Config.get ctxt Syntax.ambiguity_level;
    1.38        val limit = Config.get ctxt Syntax.ambiguity_limit;
    1.39  
    1.40 -      fun ambig_msg () =
    1.41 +      val ambig_msg =
    1.42          if ambiguity > 1 andalso ambiguity <= level then
    1.43 -          "Got more than one parse tree.\n\
    1.44 -          \Retry with smaller syntax_ambiguity_level for more information."
    1.45 -        else "";
    1.46 +          ["Got more than one parse tree.\n\
    1.47 +          \Retry with smaller syntax_ambiguity_level for more information."]
    1.48 +        else [];
    1.49  
    1.50        (*brute-force disambiguation via type-inference*)
    1.51        fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
    1.52 @@ -377,7 +379,7 @@
    1.53      in
    1.54        if len = 0 then
    1.55          report_result ctxt pos
    1.56 -          [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
    1.57 +          [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
    1.58        else if len = 1 then
    1.59          (if ambiguity > level then
    1.60            Context_Position.if_visible ctxt warning
    1.61 @@ -386,7 +388,7 @@
    1.62          else (); report_result ctxt pos results')
    1.63        else
    1.64          report_result ctxt pos
    1.65 -          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
    1.66 +          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
    1.67              (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
    1.68                (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    1.69                map show_term (take limit checked))))))]
    1.70 @@ -685,8 +687,10 @@
    1.71          val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
    1.72          val d = if intern then Lexicon.mark_const c' else c;
    1.73        in Ast.Constant d end
    1.74 -  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T]] =
    1.75 -      Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
    1.76 +  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
    1.77 +      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
    1.78 +        handle ERROR msg =>
    1.79 +          error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos))))
    1.80    | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
    1.81  
    1.82