structure Lean.ParseImports.State : Type

• imports : Array Import
• pos : String.Pos
• error? : Option String
• isModule : Bool
• isExported : Bool
• importAll : Bool

instance Lean.ParseImports.instInhabitedState : Inhabited State

def Lean.ParseImports.Parser : Type

instance Lean.ParseImports.instInhabitedParser : Inhabited Parser

@[inline]

def Lean.ParseImports.State.setPos (s : State) (pos : String.Pos) : State

@[inline]

def Lean.ParseImports.State.mkError (s : State) (msg : String) : State

def Lean.ParseImports.State.mkEOIError (s : State) : State

@[inline]

def Lean.ParseImports.State.next (s : State) (input : String) (pos : String.Pos) : State

@[inline]

def Lean.ParseImports.State.next' (s : State) (input : String) (pos : String.Pos) (h : ¬input.atEnd pos = true) : State

partial def Lean.ParseImports.finishCommentBlock (nesting : Nat) : Parser

def Lean.ParseImports.finishCommentBlock.eoi (s : State) : State

@[specialize #[]]

partial def Lean.ParseImports.takeUntil (p : Char → Bool) : Parser

@[inline]

def Lean.ParseImports.takeWhile (p : Char → Bool) : Parser

@[inline]

def Lean.ParseImports.andthen (p q : Parser) : Parser

instance Lean.ParseImports.instAndThenParser : AndThen Parser

partial def Lean.ParseImports.whitespace : Parser

@[inline]

def Lean.ParseImports.keywordCore (k : String) (failure success : Parser) : Parser

@[specialize #[]]

partial def Lean.ParseImports.keywordCore.go (k : String) (failure success : Parser) (input : String) (s : State) (i j : String.Pos) : State

@[inline]

def Lean.ParseImports.keyword (k : String) : Parser

@[inline]

def Lean.ParseImports.isIdCont : String → State → Bool

def Lean.ParseImports.State.pushImport (i : Import) (s : State) : State

@[inline]

def Lean.ParseImports.isIdRestCold (c : Char) : Bool

@[inline]

def Lean.ParseImports.isIdRestFast (c : Char) : Bool

def Lean.ParseImports.moduleIdent : Parser

partial def Lean.ParseImports.moduleIdent.parse (input : String) (finalize : Name → Parser) (module : Name) (s : State) : State

@[specialize #[]]

partial def Lean.ParseImports.many (p : Parser) : Parser

def Lean.ParseImports.setIsExported (isExported : Bool) : Parser

def Lean.ParseImports.setImportAll (importAll : Bool) : Parser

def Lean.ParseImports.main : Parser

instance Lean.instToJsonImport_1 : ToJson Import

structure Lean.ParseImportsResult : Type

• imports : Array Import
• isModule : Bool

instance Lean.instToJsonParseImportsResult : ToJson ParseImportsResult

def Lean.parseImports' (input fileName : String) : IO ParseImportsResult

Simpler and faster version of parseImports. We use it to implement Lake.

structure Lean.PrintImportResult : Type

• result? : Option ParseImportsResult
• errors : Array String

instance Lean.instToJsonPrintImportResult : ToJson PrintImportResult

structure Lean.PrintImportsResult : Type

• imports : Array PrintImportResult

instance Lean.instToJsonPrintImportsResult : ToJson PrintImportsResult

@[export lean_print_imports_json]

def Lean.printImportsJson (fileNames : Array String) : IO Unit