clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
authorwenzelm
Mon Mar 12 13:53:26 2012 +0100 (2012-03-12)
changeset 468737a73f181cbcf
parent 46872 bad72cba8a92
child 46874 993c413746f4
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
src/Pure/type_infer_context.ML
     1.1 --- a/src/Pure/type_infer_context.ML	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/Pure/type_infer_context.ML	Mon Mar 12 13:53:26 2012 +0100
     1.3 @@ -118,18 +118,14 @@
     1.4  
     1.5  fun prepare_positions ctxt tms =
     1.6    let
     1.7 -    val visible = Context_Position.is_visible ctxt;
     1.8 -
     1.9      fun prepareT (Type (a, Ts)) ps_idx =
    1.10            let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
    1.11            in (Type (a, Ts'), ps_idx') end
    1.12        | prepareT T (ps, idx) =
    1.13            (case Term_Position.decode_positionT T of
    1.14              SOME pos =>
    1.15 -              if visible then
    1.16 -                let val U = Type_Infer.mk_param idx []
    1.17 -                in (U, ((pos, U) :: ps, idx + 1)) end
    1.18 -              else (dummyT, (ps, idx))
    1.19 +              let val U = Type_Infer.mk_param idx []
    1.20 +              in (U, ((pos, U) :: ps, idx + 1)) end
    1.21            | NONE => (T, (ps, idx)));
    1.22  
    1.23      fun prepare (Const ("_type_constraint_", T)) ps_idx =