From d0929c93cdc41cc9b77fc1f46bb65182d92396c4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 8 Mar 2019 17:17:27 +0100
Subject: [PATCH] perf(library/init/lean/frontend): make `file_map`
 construction explicit, do it only once

---
 library/init/lean/frontend.lean     | 5 +++--
 library/init/lean/parser/basic.lean | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/frontend.lean b/library/init/lean/frontend.lean
index 98450e8c0c..a5f7ee0907 100644
--- a/library/init/lean/frontend.lean
+++ b/library/init/lean/frontend.lean
@@ -19,6 +19,7 @@ do t ← parser.mk_token_trie $
     parser.tokens term.builtin_trailing_parsers,
    pure $ {
      filename := filename, input := input, tokens := t,
+     file_map := file_map.from_string input,
      command_parsers := command.builtin_command_parsers,
      leading_term_parsers := term.builtin_leading_parsers,
      trailing_term_parsers := term.builtin_trailing_parsers,
@@ -62,8 +63,8 @@ meta def run_frontend (filename input : string) (print_msg : message → except_
   | (_, except.error msg) := print_msg msg *> pure []
   | (_, except.ok (p_snap, msgs)) := do
   msgs.to_list.mfor print_msg,
-  let expander_cfg : expander_config := {filename := filename, input := input, transformers := builtin_transformers},
-  let elab_cfg : elaborator_config := {filename := filename, input := input, initial_parser_cfg := parser_cfg},
+  let expander_cfg : expander_config := {transformers := builtin_transformers, ..parser_cfg},
+  let elab_cfg : elaborator_config := {filename := filename, input := input, initial_parser_cfg := parser_cfg, ..parser_cfg},
   let opts := options.mk.set_bool `trace.as_messages tt,
   let elab_st := elaborator.mk_state elab_cfg opts,
   run_frontend_aux print_msg collect_outputs elab_cfg p_snap elab_st parser_cfg expander_cfg []
diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean
index 72b9feaf6e..97b9553073 100644
--- a/library/init/lean/parser/basic.lean
+++ b/library/init/lean/parser/basic.lean
@@ -59,7 +59,7 @@ structure parser_cache :=
 structure frontend_config :=
 (filename : string)
 (input    : string)
-(file_map : file_map := file_map.from_string input)
+(file_map : file_map)
 
 /- Remark: if we have a node in the trie with `some token_config`, the string induced by the path is equal to the `token_config.prefix`. -/
 structure parser_config extends frontend_config :=