export position_of;
authorwenzelm
Fri Mar 27 15:42:53 2009 +0100 (2009-03-27)
changeset 3074450ccaef52871
parent 30743 2c83f7eaf1a4
child 30745 2823a89c76a4
child 30747 b8ca7e450de3
export position_of;
src/Pure/ML/ml_test.ML
     1.1 --- a/src/Pure/ML/ml_test.ML	Fri Mar 27 12:22:02 2009 +0100
     1.2 +++ b/src/Pure/ML/ml_test.ML	Fri Mar 27 15:42:53 2009 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature ML_TEST =
     1.6  sig
     1.7 +  val position_of: Proof.context -> PolyML.location -> Position.T
     1.8    val eval: bool -> Position.T -> ML_Lex.token list -> unit
     1.9  end
    1.10  
    1.11 @@ -33,9 +34,9 @@
    1.12        |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
    1.13    in (regs, context') end;
    1.14  
    1.15 -fun pos_of_location context
    1.16 +fun position_of ctxt
    1.17      ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
    1.18 -  (case pairself (Inttab.lookup (Extra_Env.get context)) (i, j) of
    1.19 +  (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
    1.20      (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
    1.21    | (SOME pos, NONE) => pos
    1.22    | _ => Position.line_file line file);
    1.23 @@ -45,7 +46,7 @@
    1.24  
    1.25  fun report_parse_tree context depth =
    1.26    let
    1.27 -    val pos_of = pos_of_location context;
    1.28 +    val pos_of = position_of (Context.proof_of context);
    1.29      fun report loc (PTtype types) =
    1.30            PolyML.NameSpace.displayTypeExpression (types, depth)
    1.31            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    1.32 @@ -93,7 +94,8 @@
    1.33      fun put_message {message, hard, location, context = _} =
    1.34       (put (if hard then "Error: " else "Warning: ");
    1.35        put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
    1.36 -      put (Position.str_of (pos_of_location (the (Context.thread_data ())) location) ^ "\n"));
    1.37 +      put (Position.str_of
    1.38 +        (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n"));
    1.39  
    1.40  
    1.41      (* results *)