structure Lean.ParseImports.State : Type

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

@[implicit_reducible]

instance Lean.ParseImports.instInhabitedState : Inhabited State

def Lean.ParseImports.instInhabitedState.default : State

def Lean.ParseImports.Parser : Type

@[inline]

def Lean.ParseImports.skip : Parser

@[implicit_reducible]

instance Lean.ParseImports.instInhabitedParser : Inhabited Parser

@[inline]

def Lean.ParseImports.State.setPos (s : State) (pos : String.Pos.Raw) : 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.clearError (s : State) : State

@[inline]

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

@[inline]

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

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

@[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

@[implicit_reducible]

instance Lean.ParseImports.instAndThenParser : AndThen Parser

partial def Lean.ParseImports.whitespace : Parser

@[inline]

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

@[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

@[inline]

def Lean.ParseImports.atomic (p : Parser) : Parser

@[specialize #[]]

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

def Lean.ParseImports.setIsModule (isModule : Bool) : Parser

def Lean.ParseImports.setMeta : Parser

def Lean.ParseImports.setExported : Parser

def Lean.ParseImports.setImportAll : Parser

def Lean.ParseImports.main : Parser

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

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

structure Lean.PrintImportResult : Type

• result? : Option ModuleHeader
• errors : Array String

def Lean.instToJsonPrintImportResult.toJson : PrintImportResult → Json

@[implicit_reducible]

instance Lean.instToJsonPrintImportResult : ToJson PrintImportResult

structure Lean.PrintImportsResult : Type

• imports : Array PrintImportResult

@[implicit_reducible]

instance Lean.instToJsonPrintImportsResult : ToJson PrintImportsResult

def Lean.instToJsonPrintImportsResult.toJson : PrintImportsResult → Json

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