chore(library/init/lean): filename ==> fileName

library/init/lean/elaborator/basic.lean

@@ -233,7 +233,7 @@ def mkMessage (msg : String) (pos : Option String.Pos := none) : Elab Message :=
 do ctx ← read;
    s ← get;
    let pos := ctx.fileMap.toPosition (pos.getOrElse s.cmdPos);
-   pure { filename := ctx.fileName, pos := pos, text := msg }
+   pure { fileName := ctx.fileName, pos := pos, text := msg }
 
 def logErrorAt (pos : String.Pos) (errorMsg : String) : Elab Unit :=
 mkMessage errorMsg pos >>= logMessage
@@ -296,7 +296,7 @@ abbrev Frontend := ReaderT Parser.ParserContextCore (EState ElabException Fronte
 
 def getElabContext : Frontend ElabContext :=
 do c ← read;
-   pure { fileName := c.filename, fileMap := c.fileMap }
+   pure { fileName := c.fileName, fileMap := c.fileMap }
 
 @[specialize] def runElab {α} (x : Elab α) : Frontend α :=
 do c ← getElabContext;
@@ -373,7 +373,7 @@ catch
      env ← mkEmptyEnvironment;
      let spos := header.getPos.getOrElse 0;
      let pos  := ctx.fileMap.toPosition spos;
-     pure (env, messages.add { filename := ctx.filename, text := toString e, pos := pos }))
+     pure (env, messages.add { fileName := ctx.fileName, text := toString e, pos := pos }))
 
 def toBaseDir (fileName : Option String) : IO (Option String) :=
 match fileName with

library/init/lean/elaborator/preterm.lean

@@ -142,7 +142,7 @@ fun stx => do
   match oldElaborateAux s.env scope.options s.mctx scope.lctx p with
   | Except.error (some pos, fmt) => do
     ctx ← read;
-    logMessage { filename := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
+    logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
     throw ElabException.silent
   | Except.error (none, fmt)     => logErrorAndThrow stx (fmt.pretty scope.options)
   | Except.ok (env, mctx, e)     => do

library/init/lean/message.lean

@@ -9,15 +9,15 @@ prelude
 import init.data.tostring init.lean.position
 
 namespace Lean
-def mkErrorStringWithPos (filename : String) (line col : Nat) (msg : String) : String :=
-filename ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg
+def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : String :=
+fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg
 
 inductive MessageSeverity
 | information | warning | error
 
 -- TODO: structured messages
 structure Message :=
-(filename : String)
+(fileName : String)
 (pos      : Position)
 (endPos   : Option Position  := none)
 (severity : MessageSeverity := MessageSeverity.error)
@@ -26,7 +26,7 @@ structure Message :=
 
 namespace Message
 protected def toString (msg : Message) : String :=
-mkErrorStringWithPos msg.filename msg.pos.line msg.pos.column
+mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
  ((match msg.severity with
    | MessageSeverity.information => ""
    | MessageSeverity.warning => "warning: "
@@ -34,7 +34,7 @@ mkErrorStringWithPos msg.filename msg.pos.line msg.pos.column
   (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ msg.text)
 
 instance : Inhabited Message :=
-⟨{ filename := "", pos := ⟨0, 1⟩, text := ""}⟩
+⟨{ fileName := "", pos := ⟨0, 1⟩, text := ""}⟩
 
 instance : HasToString Message :=
 ⟨Message.toString⟩

library/init/lean/parser/module.lean

@@ -33,7 +33,7 @@ instance ModuleParserState.inhabited : Inhabited ModuleParserState :=
 
 private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
 let pos := c.fileMap.toPosition pos;
-{ filename := c.filename, pos := pos, text := errorMsg }
+{ fileName := c.fileName, pos := pos, text := errorMsg }
 
 def parseHeader (env : Environment) (c : ParserContextCore) : Syntax × ModuleParserState × MessageLog :=
 let c   := c.toParserContext env;
@@ -98,9 +98,9 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo
       testModuleParserAux s messages
 
 @[export lean.test_module_parser_core]
-def testModuleParser (env : Environment) (input : String) (filename := "<input>") (displayStx := false) : IO Bool :=
-timeit (filename ++ " parser") $ do
-  let ctx                := mkParserContextCore env input filename;
+def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
+timeit (fileName ++ " parser") $ do
+  let ctx                := mkParserContextCore env input fileName;
   let (stx, s, messages) := parseHeader env ctx;
   when displayStx (IO.println stx);
   testModuleParserAux env ctx displayStx s messages

library/init/lean/parser/parser.lean

@@ -72,12 +72,12 @@ abbrev SyntaxNodeKindSet := HashMap SyntaxNodeKind Unit
 
 structure ParserContextCore :=
 (input    : String)
-(filename : String)
+(fileName : String)
 (fileMap  : FileMap)
 (tokens   : TokenTable)
 
 instance ParserContextCore.inhabited : Inhabited ParserContextCore :=
-⟨{ input := "", filename := "", fileMap := default _, tokens := {} }⟩
+⟨{ input := "", fileName := "", fileMap := default _, tokens := {} }⟩
 
 structure ParserContext extends ParserContextCore :=
 (env      : Environment)
@@ -153,7 +153,7 @@ match s.errorMsg with
 | none     => ""
 | some msg =>
   let pos := ctx.fileMap.toPosition s.pos;
-  mkErrorStringWithPos ctx.filename pos.line pos.column (toString msg)
+  mkErrorStringWithPos ctx.fileName pos.line pos.column (toString msg)
 
 def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState :=
 match s with
@@ -1381,17 +1381,17 @@ def getSyntaxNodeKinds : IO (List SyntaxNodeKind) :=
 do s ← syntaxNodeKindSetRef.get;
    pure $ s.fold (fun ks k _ => k::ks) []
 
-def mkParserContextCore (env : Environment) (input : String) (filename : String) : ParserContextCore :=
+def mkParserContextCore (env : Environment) (input : String) (fileName : String) : ParserContextCore :=
 { input    := input,
-  filename := filename,
+  fileName := fileName,
   fileMap  := input.toFileMap,
   tokens   := tokenTableAttribute.ext.getState env }
 
 @[inline] def ParserContextCore.toParserContext (env : Environment) (ctx : ParserContextCore) : ParserContext :=
 { env := env, toParserContextCore := ctx }
 
-def mkParserContext (env : Environment) (input : String) (filename : String) : ParserContext :=
-(mkParserContextCore env input filename).toParserContext env
+def mkParserContext (env : Environment) (input : String) (fileName : String) : ParserContext :=
+(mkParserContextCore env input fileName).toParserContext env
 
 def mkParserState (input : String) : ParserState :=
 { cache := initCacheForInput input }