# HG changeset patch # User wenzelm # Date 1244145753 -7200 # Node ID 70309dc3deacf3e6c9ae8551689c4f9296b58b04 # Parent dde1b4d1c95b2a10910e0f8461f9fb19383278ba removed unused location_of; eval: actually pass location properties (via "file" field); diff -r dde1b4d1c95b -r 70309dc3deac src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Jun 04 22:01:54 2009 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Jun 04 22:02:33 2009 +0200 @@ -15,23 +15,6 @@ (* source locations *) -fun location_of pos : PolyML.location = - let - val props = Position.properties_of pos; - fun get k = the_default 0 (Properties.get_int props k); - - val loc_props = props |> fold Properties.remove - [Markup.lineN, Markup.end_lineN, Markup.columnN, Markup.end_columnN, - Markup.offsetN, Markup.end_offsetN]; - val text = Markup.markup (Markup.properties loc_props Markup.position) ""; - in - {file = text, - startLine = get Markup.lineN, - startPosition = get Markup.offsetN, - endLine = get Markup.end_lineN, - endPosition = get Markup.end_offsetN} - end; - fun position_of (loc: PolyML.location) = let val {file = text, startLine = line, startPosition = offset, @@ -83,10 +66,15 @@ (* input *) + val location_props = + Markup.markup (Markup.position |> Markup.properties + (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) ""; + val input = toks |> maps (fn tok => let val syms = Symbol.explode (ML_Lex.check_content_of tok); - val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms (ML_Lex.pos_of tok); + val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms + (Position.reset_range (ML_Lex.pos_of tok)); in ps ~~ map (String.explode o Symbol.esc) syms end); val input_buffer = ref input; @@ -164,7 +152,7 @@ PolyML.Compiler.CPNameSpace space, PolyML.Compiler.CPErrorMessageProc put_message, PolyML.Compiler.CPLineNo (fn () => ! line), - PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), + PolyML.Compiler.CPFileName location_props, PolyML.Compiler.CPLineOffset get_offset, PolyML.Compiler.CPCompilerResultFun result_fun]; val _ =