1.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Jun 04 22:01:54 2009 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Jun 04 22:02:33 2009 +0200
     1.3 @@ -15,23 +15,6 @@
     1.4  
     1.5  (* source locations *)
     1.6  
     1.7 -fun location_of pos : PolyML.location =
     1.8 -  let
     1.9 -    val props = Position.properties_of pos;
    1.10 -    fun get k = the_default 0 (Properties.get_int props k);
    1.11 -
    1.12 -    val loc_props = props |> fold Properties.remove
    1.13 -      [Markup.lineN, Markup.end_lineN, Markup.columnN, Markup.end_columnN,
    1.14 -        Markup.offsetN, Markup.end_offsetN];
    1.15 -    val text = Markup.markup (Markup.properties loc_props Markup.position) "";
    1.16 -  in
    1.17 -   {file = text,
    1.18 -    startLine = get Markup.lineN,
    1.19 -    startPosition = get Markup.offsetN,
    1.20 -    endLine = get Markup.end_lineN,
    1.21 -    endPosition = get Markup.end_offsetN}
    1.22 -  end;
    1.23 -
    1.24  fun position_of (loc: PolyML.location) =
    1.25    let
    1.26      val {file = text, startLine = line, startPosition = offset,
    1.27 @@ -83,10 +66,15 @@
    1.28  
    1.29      (* input *)
    1.30  
    1.31 +    val location_props =
    1.32 +      Markup.markup (Markup.position |> Markup.properties
    1.33 +          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) "";
    1.34 +
    1.35      val input = toks |> maps (fn tok =>
    1.36        let
    1.37          val syms = Symbol.explode (ML_Lex.check_content_of tok);
    1.38 -        val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms (ML_Lex.pos_of tok);
    1.39 +        val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms
    1.40 +          (Position.reset_range (ML_Lex.pos_of tok));
    1.41        in ps ~~ map (String.explode o Symbol.esc) syms end);
    1.42  
    1.43      val input_buffer = ref input;
    1.44 @@ -164,7 +152,7 @@
    1.45        PolyML.Compiler.CPNameSpace space,
    1.46        PolyML.Compiler.CPErrorMessageProc put_message,
    1.47        PolyML.Compiler.CPLineNo (fn () => ! line),
    1.48 -      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
    1.49 +      PolyML.Compiler.CPFileName location_props,
    1.50        PolyML.Compiler.CPLineOffset get_offset,
    1.51        PolyML.Compiler.CPCompilerResultFun result_fun];
    1.52      val _ =