# HG changeset patch # User wenzelm # Date 1245703784 -7200 # Node ID 178621145f98912a43df6852ac74ec9b71895d30 # Parent 78529fc872b10998f50632193c3101b35682f062 eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever); diff -r 78529fc872b1 -r 178621145f98 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Jun 22 20:59:33 2009 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Jun 22 22:49:44 2009 +0200 @@ -63,6 +63,8 @@ (* eval ML source tokens *) +val offset_of = the_default 0 o Position.offset_of; + fun eval verbose pos toks = let val _ = Secure.secure_mltext (); @@ -80,25 +82,24 @@ val syms = Symbol.explode (ML_Lex.check_content_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); + in + (ps ~~ syms) |> maps (fn (p, sym) => + map (pair (offset_of p)) (String.explode (Symbol.esc sym))) + end); val end_pos = if null toks then Position.none else ML_Lex.end_pos_of (List.last toks); - val input_buffer = ref (input @ [(end_pos, [#"\n"])]); + val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]); val line = ref (the_default 1 (Position.line_of pos)); - fun get_offset () = - the_default 0 - (get_first (fn (_, []) => NONE | (p, _) => Position.offset_of p) (! input_buffer)); - + fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i); fun get () = (case ! input_buffer of [] => NONE - | (_, []) :: rest => (input_buffer := rest; get ()) - | (p, c :: cs) :: rest => - (input_buffer := (p, cs) :: rest; + | (_, c) :: rest => + (input_buffer := rest; if c = #"\n" then line := ! line + 1 else (); SOME c));